Library MetaCoq.Template.Reflect

From Coq Require Numbers.Cyclic.Int63.Uint63 Floats.PrimFloat Floats.FloatAxioms.
From MetaCoq.Template Require Import utils BasicAst Universes Kernames.
Require Import ssreflect.
From Equations Require Import Equations.

#[program,global] Instance reflect_prim_int : ReflectEq Numbers.Cyclic.Int63.Uint63.int :=
  { eqb := Numbers.Cyclic.Int63.Uint63.eqb }.
Next Obligation.
  destruct (Uint63.eqb x y) eqn:eq; constructor.
  now apply (Numbers.Cyclic.Int63.Uint63.eqb_spec x y) in eq.
  now apply (Numbers.Cyclic.Int63.Uint63.eqb_false_spec x y) in eq.
Qed.

Derive NoConfusion EqDec for SpecFloat.spec_float.

Local Obligation Tactic := idtac.

#[program,global]
Instance reflect_prim_float : ReflectEq PrimFloat.float :=
  { eqb x y := eqb (ReflectEq := EqDec_ReflectEq SpecFloat.spec_float) (FloatOps.Prim2SF x) (FloatOps.Prim2SF y) }.
Next Obligation.
  intros. cbn -[eqb].
  destruct (eqb_spec (ReflectEq := EqDec_ReflectEq SpecFloat.spec_float) (FloatOps.Prim2SF x) (FloatOps.Prim2SF y)) as [H|H]; constructor.
  now apply FloatAxioms.Prim2SF_inj.
  intros e; apply H. rewrite e.
  reflexivity.
Qed.

Definition eq_prop_level l1 l2 :=
  match l1, l2 with
  | PropLevel.lProp, PropLevel.lProptrue
  | PropLevel.lSProp, PropLevel.lSProptrue
  | _, _false
  end.

#[global, program] Instance reflect_prop_level : ReflectEq PropLevel.t := {
  eqb := eq_prop_level
}.
Next Obligation.
  destruct x, y.
  all: unfold eq_prop_level.
  all: try solve [ constructor ; reflexivity ].
  all: try solve [ constructor ; discriminate ].
Qed.

Definition eq_levels (l1 l2 : PropLevel.t + Level.t) :=
  match l1, l2 with
  | inl l, inl l'eqb l l'
  | inr l, inr l'eqb l l'
  | _, _false
  end.

#[global, program] Instance reflect_levels : ReflectEq (PropLevel.t + Level.t) := {
  eqb := eq_levels
}.
Next Obligation.
  destruct x, y.
  cbn -[eqb]. destruct (eqb_spec t t0). subst. now constructor.
  all:try (constructor; cong).
  cbn -[eqb]. destruct (eqb_spec t t0). subst; now constructor.
  constructor; cong.
Qed.

Definition eq_name na nb :=
  match na, nb with
  | nAnon, nAnontrue
  | nNamed a, nNamed beqb a b
  | _, _false
  end.

#[global, program] Instance reflect_name : ReflectEq name := {
  eqb := eq_name
}.
Next Obligation.
  intros x y. destruct x, y.
  - cbn. constructor. reflexivity.
  - cbn. constructor. discriminate.
  - cbn. constructor. discriminate.
  - unfold eq_name. destruct (eqb_spec i i0); nodec.
    constructor. f_equal. assumption.
Qed.

Definition eq_relevance r r' :=
  match r, r' with
  | Relevant, Relevanttrue
  | Irrelevant, Irrelevanttrue
  | _, _false
  end.

#[global, program] Instance reflect_relevance : ReflectEq relevance := {
  eqb := eq_relevance
}.
Next Obligation.
  intros x y. destruct x, y.
  - cbn. constructor. reflexivity.
  - cbn. constructor. discriminate.
  - cbn. constructor. discriminate.
  - simpl. now constructor.
Qed.

Definition eq_aname (na nb : binder_annot name) :=
  eqb na.(binder_name) nb.(binder_name) &&
  eqb na.(binder_relevance) nb.(binder_relevance).

#[global, program] Instance reflect_aname : ReflectEq aname := {
  eqb := eq_aname
}.
Next Obligation.
  intros x y. unfold eq_aname.
  destruct (eqb_spec x.(binder_name) y.(binder_name));
  destruct (eqb_spec x.(binder_relevance) y.(binder_relevance));
  constructor; destruct x, y; simpl in *; cong.
Qed.

Definition eq_def {A} `{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.

#[global, program] Instance reflect_def : {A} `{ReflectEq A}, ReflectEq (def A) := {
  eqb := eq_def
}.
Next Obligation.
  intros A RA.
  intros x y. destruct x as [n1 t1 b1 a1], y as [n2 t2 b2 a2].
  unfold eq_def.
  destruct (eqb_spec n1 n2) ; nodec.
  destruct (eqb_spec t1 t2) ; nodec.
  destruct (eqb_spec b1 b2) ; nodec.
  destruct (eqb_spec a1 a2) ; nodec.
  cbn. constructor. subst. reflexivity.
Qed.

Definition eq_cast_kind (c c' : cast_kind) : bool :=
  match c, c' with
  | VmCast, VmCast
  | NativeCast, NativeCast
  | Cast, Casttrue
  | _, _false
  end.

#[global, program] Instance reflect_cast_kind : ReflectEq cast_kind :=
  { eqb := eq_cast_kind }.
Next Obligation.
  induction x, y. all: cbn. all: nodec.
  all: left. all: reflexivity.
Qed.

Definition eqb_case_info
  (ci ci' : BasicAst.case_info) :=
  let (ci_ind, ci_npar, ci_relevance) := ci in
  let (ci_ind', ci_npar', ci_relevance') := ci' in
  eqb ci_ind ci_ind' && eqb ci_npar ci_npar' && eqb ci_relevance ci_relevance'.

#[global, program] Instance reflect_case_info : ReflectEq case_info :=
  {| eqb := eqb_case_info |}.
Next Obligation.
  intros. destruct x as [ci_ind ci_npar ci_relevance], y as [ci_ind' ci_npar' ci_relevance']. cbn -[eqb].
  destruct (eqb_spec ci_ind ci_ind'); subst;
  destruct (eqb_spec ci_npar ci_npar'); subst;
    destruct (eqb_spec ci_relevance ci_relevance'); subst; constructor; congruence.
Qed.

Derive NoConfusion NoConfusionHom for sig.
Derive NoConfusion NoConfusionHom for prod.

Definition eqb_context_decl {term : Type} (eqterm : term term bool)
  (x y : BasicAst.context_decl term) :=
  let (na, b, ty) := x in
  let (na', b', ty') := y in
  eqb na na' && eq_option eqterm b b' && eqterm ty ty'.

#[global, program] Instance eq_decl_reflect {term} {Ht : ReflectEq term} : ReflectEq (BasicAst.context_decl term) :=
  {| eqb := eqb_context_decl eqb |}.
Next Obligation.
  intros. destruct x as [na b ty], y as [na' b' ty']. cbn -[eqb].
  change (eq_option eqb b b') with (eqb b b').
  destruct (eqb_spec na na'); subst;
    destruct (eqb_spec b b'); subst;
      destruct (eqb_spec ty ty'); subst; constructor; congruence.
Qed.

Definition eqb_recursivity_kind r r' :=
  match r, r' with
  | Finite, Finitetrue
  | CoFinite, CoFinitetrue
  | BiFinite, BiFinitetrue
  | _, _false
  end.

#[global] Instance reflect_recursivity_kind : ReflectEq recursivity_kind.
Proof.
  refine {| eqb := eqb_recursivity_kind |}.
  destruct x, y; simpl; constructor; congruence.
Defined.

Definition eqb_ConstraintType x y :=
  match x, y with
  | ConstraintType.Le n, ConstraintType.Le mZ.eqb n m
  | ConstraintType.Eq, ConstraintType.Eqtrue
  | _, _false
  end.

#[global] Instance reflect_ConstraintType : ReflectEq ConstraintType.t.
Proof.
  refine {| eqb := eqb_ConstraintType |}.
  destruct x, y; simpl; try constructor; try congruence.
  destruct (Z.eqb_spec z z0); constructor. now subst.
  cong.
Defined.

#[global, program] Instance Z_as_int : ReflectEq Int.Z_as_Int.t :=
  { eqb := Z.eqb }.
Next Obligation.
  apply (reflect_reflectProp_2 Z.eqb_spec).
Qed.

Scheme level_lt_ind_dep := Induction for Level.lt_ Sort Prop.
Scheme constraint_type_lt_ind_dep := Induction for ConstraintType.lt_ Sort Prop.
Scheme constraint_lt_ind_dep := Induction for UnivConstraint.lt_ Sort Prop.
Derive Signature for UnivConstraint.lt_.
Derive Signature for le.
Set Equations With UIP.

Derive NoConfusion EqDec for comparison.

Lemma string_compare_irrel {s s'} {c} (H H' : string_compare s s' = c) : H = H'.
Proof.
  apply uip.
Qed.

Scheme le_ind_prop := Induction for le Sort Prop.

Lemma nat_le_irrel {x y : nat} (l l' : x y) : l = l'.
Proof.
  induction l using le_ind_prop; depelim l'.
  - reflexivity.
  - lia.
  - lia.
  - f_equal. apply IHl.
Qed.

Lemma lt_level_irrel {x y : Level.t} (l l' : Level.lt_ x y) : l = l'.
Proof.
  induction l using level_lt_ind_dep; depelim l'; auto.
  - now replace l with l0 by apply uip.
  - f_equal. apply nat_le_irrel.
Qed.

Lemma constraint_type_lt_level_irrel {x y} (l l' : ConstraintType.lt_ x y) : l = l'.
Proof.
  induction l using constraint_type_lt_ind_dep; depelim l'; auto.
  f_equal. apply uip.
Qed.

Require Import RelationClasses.

Lemma constraint_lt_irrel (x y : UnivConstraint.t) (l l' : UnivConstraint.lt_ x y) : l = l'.
Proof.
  revert l'. induction l using constraint_lt_ind_dep.
  - intros l'. depelim l'.
    now rewrite (lt_level_irrel l l4).
    now elim (irreflexivity (R:=ConstraintType.lt) l4).
    now elim (irreflexivity l4).
  - intros l'; depelim l'.
    now elim (irreflexivity (R:=ConstraintType.lt) l).
    now rewrite (constraint_type_lt_level_irrel l l4).
    now elim (irreflexivity l4).
  - intros l'; depelim l'.
    now elim (irreflexivity l).
    now elim (irreflexivity l).
    now rewrite (lt_level_irrel l l4).
Qed.

Module LevelSetsUIP.
  Import LevelSet.Raw.

  Fixpoint levels_tree_eqb (x y : LevelSet.Raw.t) :=
  match x, y with
  | LevelSet.Raw.Leaf, LevelSet.Raw.Leaftrue
  | LevelSet.Raw.Node h l o r, LevelSet.Raw.Node h' l' o' r'
    eqb h h' && levels_tree_eqb l l' && eqb o o' && levels_tree_eqb r r'
  | _, _false
  end.

  Scheme levels_tree_rect := Induction for LevelSet.Raw.tree Sort Type.

  #[global, program] Instance levels_tree_reflect : ReflectEq LevelSet.Raw.t :=
   {| eqb := levels_tree_eqb |}.
  Next Obligation.
    induction x using levels_tree_rect; destruct y; try constructor; auto; try congruence.
    cbn [levels_tree_eqb].
    destruct (eqb_spec t0 t2); try constructor; auto; try congruence.
    destruct (IHx1 y1); try constructor; auto; try congruence.
    destruct (eqb_spec t1 t3); try constructor; auto; try congruence.
    destruct (IHx2 y2); try constructor; auto; try congruence.
  Qed.

  Derive NoConfusion for LevelSet.Raw.tree.
  Derive Signature for LevelSet.Raw.bst.

  Definition eqb_LevelSet x y :=
    eqb (LevelSet.this x) (LevelSet.this y).

  Lemma ok_irrel (x : t) (o o' : Ok x) : o = o'.
  Proof.
    unfold Ok in ×.
    induction o.
    - now depelim o'.
    - depelim o'. f_equal; auto.
      clear -l0 l2. red in l0, l2.
      extensionality y. extensionality inl.
      apply lt_level_irrel.
      extensionality y. extensionality inl.
      apply lt_level_irrel.
  Qed.

  #[global,program] Instance reflect_LevelSet : ReflectEq LevelSet.t :=
   {| eqb := eqb_LevelSet |}.
  Next Obligation.
    intros [thisx okx] [thisy oky].
    unfold eqb_LevelSet.
    cbn -[eqb].
    destruct (eqb_spec thisx thisy); subst; constructor.
    - f_equal. apply ok_irrel.
    - congruence.
  Qed.
End LevelSetsUIP.

Module ConstraintSetsUIP.
  Import ConstraintSet.Raw.

  Fixpoint cs_tree_eqb (x y : t) :=
    match x, y with
    | ConstraintSet.Raw.Leaf, ConstraintSet.Raw.Leaftrue
    | ConstraintSet.Raw.Node h l o r, ConstraintSet.Raw.Node h' l' o' r'
      eqb h h' && cs_tree_eqb l l' && eqb o o' && cs_tree_eqb r r'
    | _, _false
    end.

  Scheme cs_tree_rect := Induction for ConstraintSet.Raw.tree Sort Type.

  #[global,program] Instance cs_tree_reflect : ReflectEq ConstraintSet.Raw.t :=
   {| eqb := cs_tree_eqb |}.
  Next Obligation.
    induction x using cs_tree_rect; destruct y; try constructor; auto; try congruence.
    cbn [cs_tree_eqb].
    destruct (eqb_spec t0 t1); try constructor; auto; try congruence.
    destruct (IHx1 y1); try constructor; auto; try congruence.
    destruct (eqb_spec p p0); try constructor; auto; try congruence.
    destruct (IHx2 y2); try constructor; auto; try congruence.
  Qed.

  Definition eqb_ConstraintSet x y :=
    eqb (ConstraintSet.this x) (ConstraintSet.this y).

  Derive NoConfusion for ConstraintSet.Raw.tree.
  Derive Signature for ConstraintSet.Raw.bst.

  Lemma ok_irrel (x : t) (o o' : Ok x) : o = o'.
  Proof.
    unfold Ok in ×.
    induction o.
    - now depelim o'.
    - depelim o'. f_equal; auto.
      clear -l0 l2. red in l0, l2.
      extensionality y. extensionality inl.
      apply constraint_lt_irrel.
      extensionality y. extensionality inl.
      apply constraint_lt_irrel.
  Qed.

  #[global,program] Instance reflect_ConstraintSet : ReflectEq ConstraintSet.t :=
   {| eqb := eqb_ConstraintSet |}.
  Next Obligation.
    intros [thisx okx] [thisy oky].
    unfold eqb_ConstraintSet. cbn.
    cbn -[eqb].
    destruct (eqb_spec thisx thisy); subst; constructor.
    - f_equal. apply ok_irrel.
    - congruence.
  Qed.

End ConstraintSetsUIP.

Ltac finish_reflect :=
  (repeat
    match goal with
    | |- context[eqb ?a ?b] ⇒ destruct (eqb_spec a b); [subst|constructor; congruence]
    end);
  constructor; trivial; congruence.

Definition eqb_universes_decl x y :=
  match x, y with
  | Monomorphic_ctx, Monomorphic_ctxtrue
  | Polymorphic_ctx cx, Polymorphic_ctx cyeqb cx cy
  | _, _false
  end.

#[global,program] Instance reflect_universes_decl : ReflectEq universes_decl :=
 {| eqb := eqb_universes_decl |}.
 Next Obligation.
   unfold eqb_universes_decl.
   intros [] []; finish_reflect.
Qed.

Definition eqb_allowed_eliminations x y :=
  match x, y with
  | IntoSProp, IntoSProp
  | IntoPropSProp, IntoPropSProp
  | IntoSetPropSProp, IntoSetPropSProp
  | IntoAny, IntoAnytrue
  | _, _false
  end.

#[global,program] Instance reflect_allowed_eliminations : ReflectEq allowed_eliminations :=
 {| eqb := eqb_allowed_eliminations |}.
Next Obligation.
 intros [] []; simpl; constructor; congruence.
Qed.

Local Infix "==?" := eqb (at level 20).

Definition eqb_Variance x y :=
  match x, y with
  | Variance.Irrelevant, Variance.Irrelevant
  | Variance.Covariant, Variance.Covariant
  | Variance.Invariant, Variance.Invarianttrue
  | _, _false
  end.

#[global,program] Instance reflect_Variance : ReflectEq Variance.t :=
 {| eqb := eqb_Variance |}.
Next Obligation.
  intros [] []; constructor; congruence.
Qed.