Library MetaCoq.PCUIC.PCUICReflect

Inductive reflectT (A : Type) : bool → Type :=
| ReflectT : A → reflectT A true
| ReflectF : (A → False) → reflectT A false.

Lemma reflectT_reflect (A : Prop) b : reflectT A b → reflect A b.

Lemma reflect_reflectT (A : Prop) b : reflect A b → reflectT A b.


Class ReflectEq A := {
  eqb : A → A → bool ;
  eqb_spec : ∀ x y : A, reflect (x = y) (eqb x y)
}.

Instance ReflectEq_EqDec :
  ∀ A, ReflectEq A → EqDec A.

Definition eq_dec_to_bool {A} `{EqDec A} x y :=
  match eq_dec x y with
  | left _ ⇒ true
  | right _ ⇒ false
  end.

Lemma EqDec_ReflectEq : ∀ A `{EqDec A}, ReflectEq A.


Definition eq_option {A} `{ReflectEq A} (u v : option A) : bool :=
  match u, v with
  | Some u, Some v ⇒ eqb u v
  | None, None ⇒ true
  | _, _ ⇒ false
  end.

Instance reflect_option : ∀ {A}, ReflectEq A → ReflectEq (option A) := {
  eqb := eq_option
}.

Fixpoint eq_list {A} (eqA : A → A → bool) (l l' : list A) : bool :=
  match l, l' with
  | a :: l, a' :: l' ⇒
    if eqA a a' then eq_list eqA l l'
    else false
  | [], [] ⇒ true
  | _, _ ⇒ false
  end.

Instance reflect_list : ∀ {A}, ReflectEq A → ReflectEq (list A) := {
  eqb := eq_list eqb
}.

Instance reflect_string : ReflectEq string := {
  eqb := eq_string
}.

Instance reflect_nat : ReflectEq nat := {
  eqb_spec := Nat.eqb_spec
}.

Definition eq_level l1 l2 :=
  match l1, l2 with
  | Level.lProp, Level.lProp ⇒ true
  | Level.lSet, Level.lSet ⇒ true
  | Level.Level s1, Level.Level s2 ⇒ eqb s1 s2
  | Level.Var n1, Level.Var n2 ⇒ eqb n1 n2
  | _, _ ⇒ false
  end.

Instance reflect_level : ReflectEq Level.t := {
  eqb := eq_level
}.

Definition eq_prod {A B} (eqA : A → A → bool) (eqB : B → B → bool) x y :=
  let '(a1, b1) := x in
  let '(a2, b2) := y in
  if eqA a1 a2 then eqB b1 b2
  else false.

Instance reflect_prod : ∀ {A B}, ReflectEq A → ReflectEq B → ReflectEq (A × B) := {
  eqb := eq_prod eqb eqb
}.

Definition eq_bool b1 b2 : bool :=
  if b1 then b2 else negb b2.

Instance reflect_bool : ReflectEq bool := {
  eqb := eq_bool
}.

Definition eq_name na nb :=
  match na, nb with
  | nAnon, nAnon ⇒ true
  | nNamed a, nNamed b ⇒ eqb a b
  | _, _ ⇒ false
  end.

Instance reflect_name : ReflectEq name := {
  eqb := eq_name
}.

Definition eq_inductive ind ind' :=
  match ind, ind' with
  | mkInd m n, mkInd m' n' ⇒
    eqb m m' && eqb n n'
  end.

Instance reflect_inductive : ReflectEq inductive := {
  eqb := eq_inductive
}.

Lemma eq_inductive_refl i : eq_inductive i i.

Definition eq_def {A : Set} `{ReflectEq A} (d1 d2 : def A) : bool :=
  match d1, d2 with
  | mkdef n1 t1 b1 a1, mkdef n2 t2 b2 a2 ⇒
    eqb n1 n2 && eqb t1 t2 && eqb b1 b2 && eqb a1 a2
  end.

Instance reflect_def : ∀ {A : Set} `{ReflectEq A}, ReflectEq (def A) := {
  eqb := eq_def
}.

Fixpoint eq_non_empty_list {A : Set} (eqA : A → A → bool) (l l' : non_empty_list A) : bool :=
  match l, l' with
  | NEL.sing a, NEL.sing a' ⇒ eqA a a'
  | NEL.cons a l, NEL.cons a' l' ⇒
    eqA a a' && eq_non_empty_list eqA l l'
  | _, _ ⇒ false
  end.

Instance reflect_non_empty_list :
  ∀ {A : Set} `{ReflectEq A}, ReflectEq (non_empty_list A) :=
  { eqb := eq_non_empty_list eqb }.






Instance reflect_term : ReflectEq term :=
  let h := EqDec_ReflectEq term in _.

Definition eq_sig_true {A f} `{ReflectEq A} (x y : { z : A | f z = true }) : bool :=
  let '(exist x hx) := x in
  let '(exist y hy) := y in
  eqb x y.

Instance reflect_sig_true {A f} `{ReflectEq A} : ReflectEq ({ z : A | f z = true }) := {
  eqb := eq_sig_true
}.


Definition eqb_context_decl (x y : context_decl) :=
  let (na, b, ty) := x in
  let (na', b', ty') := y in
  eqb na na' && eqb b b' && eqb ty ty'.

Instance eq_ctx : ReflectEq context_decl.

Instance eqb_ctx : ReflectEq context := _.