Library MetaCoq.Template.ReflectAst
From Coq Require Numbers.Cyclic.Int63.Uint63 Floats.PrimFloat Floats.FloatAxioms.
From MetaCoq.Template Require Import utils AstUtils BasicAst Ast Reflect Environment Induction.
Require Import ssreflect.
From Equations Require Import Equations.
Local Infix "==?" := eqb (at level 20).
Local Ltac finish :=
let h := fresh "h" in
right ;
match goal with
| e : ?t ≠ ?u |- _ ⇒
intro h ; apply e ; now inversion h
end.
Local Ltac fcase c :=
let e := fresh "e" in
case c ; intro e ; [ subst ; try (left ; reflexivity) | finish ].
Local Ltac term_dec_tac term_dec :=
repeat match goal with
| t : term, u : term |- _ ⇒ fcase (term_dec t u)
| u : Universe.t, u' : Universe.t |- _ ⇒ fcase (eq_dec u u')
| x : Instance.t, y : Instance.t |- _ ⇒
fcase (eq_dec x y)
| x : list Level.t, y : Instance.t |- _ ⇒
fcase (eq_dec x y)
| x : list aname, y : list aname |- _ ⇒
fcase (eq_dec x y)
| n : nat, m : nat |- _ ⇒ fcase (Nat.eq_dec n m)
| i : ident, i' : ident |- _ ⇒ fcase (eq_dec i i')
| i : kername, i' : kername |- _ ⇒ fcase (eq_dec i i')
| i : string, i' : kername |- _ ⇒ fcase (eq_dec i i')
| n : name, n' : name |- _ ⇒ fcase (eq_dec n n')
| n : aname, n' : aname |- _ ⇒ fcase (eq_dec n n')
| i : inductive, i' : inductive |- _ ⇒ fcase (eq_dec i i')
| x : inductive × nat, y : inductive × nat |- _ ⇒
fcase (eq_dec x y)
| x : case_info, y : case_info |- _ ⇒
fcase (eq_dec x y)
| x : projection, y : projection |- _ ⇒ fcase (eq_dec x y)
| x : cast_kind, y : cast_kind |- _ ⇒ fcase (eq_dec x y)
end.
#[global] Instance eq_predicate {term} `{EqDec term} : EqDec (predicate term).
Proof.
intros [] [].
fcase (eq_dec pparams pparams0).
fcase (eq_dec puinst puinst0).
fcase (eq_dec pcontext pcontext0).
fcase (eq_dec preturn preturn0).
Defined.
Derive NoConfusion NoConfusionHom for term.
#[global] Instance EqDec_term : EqDec term.
Proof.
intro x; induction x using term_forall_list_rect ; intro t ;
destruct t ; try (right ; discriminate).
all: term_dec_tac term_dec.
- induction X in args |- ×.
+ destruct args.
× left. reflexivity.
× right. discriminate.
+ destruct args.
× right. discriminate.
× destruct (IHX args) ; nodec.
destruct (p t) ; nodec.
subst. left. inversion e. reflexivity.
- destruct (IHx1 t1) ; nodec.
destruct (IHx2 t2) ; nodec.
subst. left. reflexivity.
- destruct (IHx1 t1) ; nodec.
destruct (IHx2 t2) ; nodec.
subst. left. reflexivity.
- destruct (IHx1 t1) ; nodec.
destruct (IHx2 t2) ; nodec.
subst. left. reflexivity.
- destruct (IHx1 t1) ; nodec.
destruct (IHx2 t2) ; nodec.
destruct (IHx3 t3) ; nodec.
subst. left. reflexivity.
- destruct (IHx t) ; nodec.
subst. induction X in args |- ×.
+ destruct args. all: nodec.
left. reflexivity.
+ destruct args. all: nodec.
destruct (IHX args). all: nodec.
destruct (p t0). all: nodec.
subst. inversion e. subst.
left. reflexivity.
- destruct (IHx t) ; nodec.
destruct p0, type_info; subst; cbn.
term_dec_tac term_dec.
destruct X as (?&?).
destruct (s preturn0); cbn in × ; nodec.
subst.
assert ({pparams = pparams0} + {pparams ≠ pparams0}) as []; nodec.
{ revert pparams0.
clear -a.
induction a.
- intros []; [left; reflexivity|right; discriminate].
- intros []; [right; discriminate|].
destruct (p t) ; nodec.
destruct (IHa l0) ; nodec.
subst; left; reflexivity. }
subst.
revert branches. clear -X0.
induction X0 ; intro l0.
+ destruct l0.
× left. reflexivity.
× right. discriminate.
+ destruct l0.
× right. discriminate.
× destruct (IHX0 l0) ; nodec.
destruct (p (bbody b)) ; nodec.
destruct (eq_dec (bcontext x) (bcontext b)) ; nodec.
destruct x, b.
left.
cbn in ×. subst. inversion e. reflexivity.
- destruct (IHx t) ; nodec.
left. subst. reflexivity.
- revert mfix. induction X ; intro m0.
+ destruct m0.
× left. reflexivity.
× right. discriminate.
+ destruct p as [p1 p2].
destruct m0.
× right. discriminate.
× destruct (p1 (dtype d)) ; nodec.
destruct (p2 (dbody d)) ; nodec.
destruct (IHX m0) ; nodec.
destruct x, d ; subst. cbn in ×.
destruct (eq_dec dname dname0) ; nodec.
subst. inversion e1. subst.
destruct (eq_dec rarg rarg0) ; nodec.
subst. left. reflexivity.
- revert mfix. induction X ; intro m0.
+ destruct m0.
× left. reflexivity.
× right. discriminate.
+ destruct p as [p1 p2].
destruct m0.
× right. discriminate.
× destruct (p1 (dtype d)) ; nodec.
destruct (p2 (dbody d)) ; nodec.
destruct (IHX m0) ; nodec.
destruct x, d ; subst. cbn in ×.
destruct (eq_dec dname dname0) ; nodec.
subst. inversion e1. subst.
destruct (eq_dec rarg rarg0) ; nodec.
subst. left. reflexivity.
Defined.
#[global] Instance reflect_term : ReflectEq term :=
let h := EqDec_ReflectEq term in _.
#[global] Instance eqb_ctx : ReflectEq context := _.
From MetaCoq.Template Require Import utils AstUtils BasicAst Ast Reflect Environment Induction.
Require Import ssreflect.
From Equations Require Import Equations.
Local Infix "==?" := eqb (at level 20).
Local Ltac finish :=
let h := fresh "h" in
right ;
match goal with
| e : ?t ≠ ?u |- _ ⇒
intro h ; apply e ; now inversion h
end.
Local Ltac fcase c :=
let e := fresh "e" in
case c ; intro e ; [ subst ; try (left ; reflexivity) | finish ].
Local Ltac term_dec_tac term_dec :=
repeat match goal with
| t : term, u : term |- _ ⇒ fcase (term_dec t u)
| u : Universe.t, u' : Universe.t |- _ ⇒ fcase (eq_dec u u')
| x : Instance.t, y : Instance.t |- _ ⇒
fcase (eq_dec x y)
| x : list Level.t, y : Instance.t |- _ ⇒
fcase (eq_dec x y)
| x : list aname, y : list aname |- _ ⇒
fcase (eq_dec x y)
| n : nat, m : nat |- _ ⇒ fcase (Nat.eq_dec n m)
| i : ident, i' : ident |- _ ⇒ fcase (eq_dec i i')
| i : kername, i' : kername |- _ ⇒ fcase (eq_dec i i')
| i : string, i' : kername |- _ ⇒ fcase (eq_dec i i')
| n : name, n' : name |- _ ⇒ fcase (eq_dec n n')
| n : aname, n' : aname |- _ ⇒ fcase (eq_dec n n')
| i : inductive, i' : inductive |- _ ⇒ fcase (eq_dec i i')
| x : inductive × nat, y : inductive × nat |- _ ⇒
fcase (eq_dec x y)
| x : case_info, y : case_info |- _ ⇒
fcase (eq_dec x y)
| x : projection, y : projection |- _ ⇒ fcase (eq_dec x y)
| x : cast_kind, y : cast_kind |- _ ⇒ fcase (eq_dec x y)
end.
#[global] Instance eq_predicate {term} `{EqDec term} : EqDec (predicate term).
Proof.
intros [] [].
fcase (eq_dec pparams pparams0).
fcase (eq_dec puinst puinst0).
fcase (eq_dec pcontext pcontext0).
fcase (eq_dec preturn preturn0).
Defined.
Derive NoConfusion NoConfusionHom for term.
#[global] Instance EqDec_term : EqDec term.
Proof.
intro x; induction x using term_forall_list_rect ; intro t ;
destruct t ; try (right ; discriminate).
all: term_dec_tac term_dec.
- induction X in args |- ×.
+ destruct args.
× left. reflexivity.
× right. discriminate.
+ destruct args.
× right. discriminate.
× destruct (IHX args) ; nodec.
destruct (p t) ; nodec.
subst. left. inversion e. reflexivity.
- destruct (IHx1 t1) ; nodec.
destruct (IHx2 t2) ; nodec.
subst. left. reflexivity.
- destruct (IHx1 t1) ; nodec.
destruct (IHx2 t2) ; nodec.
subst. left. reflexivity.
- destruct (IHx1 t1) ; nodec.
destruct (IHx2 t2) ; nodec.
subst. left. reflexivity.
- destruct (IHx1 t1) ; nodec.
destruct (IHx2 t2) ; nodec.
destruct (IHx3 t3) ; nodec.
subst. left. reflexivity.
- destruct (IHx t) ; nodec.
subst. induction X in args |- ×.
+ destruct args. all: nodec.
left. reflexivity.
+ destruct args. all: nodec.
destruct (IHX args). all: nodec.
destruct (p t0). all: nodec.
subst. inversion e. subst.
left. reflexivity.
- destruct (IHx t) ; nodec.
destruct p0, type_info; subst; cbn.
term_dec_tac term_dec.
destruct X as (?&?).
destruct (s preturn0); cbn in × ; nodec.
subst.
assert ({pparams = pparams0} + {pparams ≠ pparams0}) as []; nodec.
{ revert pparams0.
clear -a.
induction a.
- intros []; [left; reflexivity|right; discriminate].
- intros []; [right; discriminate|].
destruct (p t) ; nodec.
destruct (IHa l0) ; nodec.
subst; left; reflexivity. }
subst.
revert branches. clear -X0.
induction X0 ; intro l0.
+ destruct l0.
× left. reflexivity.
× right. discriminate.
+ destruct l0.
× right. discriminate.
× destruct (IHX0 l0) ; nodec.
destruct (p (bbody b)) ; nodec.
destruct (eq_dec (bcontext x) (bcontext b)) ; nodec.
destruct x, b.
left.
cbn in ×. subst. inversion e. reflexivity.
- destruct (IHx t) ; nodec.
left. subst. reflexivity.
- revert mfix. induction X ; intro m0.
+ destruct m0.
× left. reflexivity.
× right. discriminate.
+ destruct p as [p1 p2].
destruct m0.
× right. discriminate.
× destruct (p1 (dtype d)) ; nodec.
destruct (p2 (dbody d)) ; nodec.
destruct (IHX m0) ; nodec.
destruct x, d ; subst. cbn in ×.
destruct (eq_dec dname dname0) ; nodec.
subst. inversion e1. subst.
destruct (eq_dec rarg rarg0) ; nodec.
subst. left. reflexivity.
- revert mfix. induction X ; intro m0.
+ destruct m0.
× left. reflexivity.
× right. discriminate.
+ destruct p as [p1 p2].
destruct m0.
× right. discriminate.
× destruct (p1 (dtype d)) ; nodec.
destruct (p2 (dbody d)) ; nodec.
destruct (IHX m0) ; nodec.
destruct x, d ; subst. cbn in ×.
destruct (eq_dec dname dname0) ; nodec.
subst. inversion e1. subst.
destruct (eq_dec rarg rarg0) ; nodec.
subst. left. reflexivity.
Defined.
#[global] Instance reflect_term : ReflectEq term :=
let h := EqDec_ReflectEq term in _.
#[global] Instance eqb_ctx : ReflectEq context := _.