350 lines
13 KiB
Coq
350 lines
13 KiB
Coq
From Equations Require Import Equations.
|
|
Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
|
|
Require Import Logic.PropExtensionality (propositional_extensionality).
|
|
Require Import ssreflect ssrbool.
|
|
Import Logic (inspect).
|
|
From Ltac2 Require Import Ltac2.
|
|
Import Ltac2.Constr.
|
|
Set Default Proof Mode "Classic".
|
|
|
|
|
|
Require Import ssreflect ssrbool.
|
|
From Hammer Require Import Tactics.
|
|
|
|
Ltac2 destruct_algo () :=
|
|
lazy_match! goal with
|
|
| [h : algo_dom ?a ?b |- _ ] =>
|
|
if is_var a then destruct $a; ltac1:(done) else
|
|
(if is_var b then destruct $b; ltac1:(done) else ())
|
|
end.
|
|
|
|
|
|
Ltac check_equal_triv :=
|
|
intros;subst;
|
|
lazymatch goal with
|
|
(* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
|
|
| [h : algo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo))
|
|
| _ => idtac
|
|
end.
|
|
|
|
Ltac solve_check_equal :=
|
|
try solve [intros *;
|
|
match goal with
|
|
| [|- _ = _] => sauto
|
|
| _ => idtac
|
|
end].
|
|
|
|
Global Set Transparent Obligations.
|
|
|
|
Local Obligation Tactic := try solve [check_equal_triv | sfirstorder].
|
|
|
|
Program Fixpoint check_equal (a b : PTm) (h : algo_dom a b) {struct h} : bool :=
|
|
match a, b with
|
|
| VarPTm i, VarPTm j => nat_eqdec i j
|
|
| PAbs a, PAbs b => check_equal_r a b _
|
|
| PAbs a, VarPTm _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
|
|
| PAbs a, PApp _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
|
|
| PAbs a, PInd _ _ _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
|
|
| PAbs a, PProj _ _ => check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) _
|
|
| VarPTm _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
|
|
| PApp _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
|
|
| PProj _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
|
|
| PInd _ _ _ _, PAbs b => check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b _
|
|
| PPair a0 b0, PPair a1 b1 =>
|
|
check_equal_r a0 a1 _ && check_equal_r b0 b1 _
|
|
| PPair a0 b0, VarPTm _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
|
|
| PPair a0 b0, PProj _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
|
|
| PPair a0 b0, PApp _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
|
|
| PPair a0 b0, PInd _ _ _ _ => check_equal_r a0 (PProj PL b) _ && check_equal_r b0 (PProj PR b) _
|
|
| VarPTm _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
|
|
| PApp _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
|
|
| PProj _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
|
|
| PInd _ _ _ _, PPair a1 b1 => check_equal_r (PProj PL a) a1 _ && check_equal_r (PProj PR a) b1 _
|
|
| PNat, PNat => true
|
|
| PZero, PZero => true
|
|
| PSuc a, PSuc b => check_equal_r a b _
|
|
| PProj p0 a, PProj p1 b => PTag_eqdec p0 p1 && check_equal a b _
|
|
| PApp a0 b0, PApp a1 b1 => check_equal a0 a1 _ && check_equal_r b0 b1 _
|
|
| PInd P0 u0 b0 c0, PInd P1 u1 b1 c1 =>
|
|
check_equal_r P0 P1 _ && check_equal u0 u1 _ && check_equal_r b0 b1 _ && check_equal_r c0 c1 _
|
|
| PUniv i, PUniv j => nat_eqdec i j
|
|
| PBind p0 A0 B0, PBind p1 A1 B1 => BTag_eqdec p0 p1 && check_equal_r A0 A1 _ && check_equal_r B0 B1 _
|
|
| _, _ => false
|
|
end
|
|
with check_equal_r (a b : PTm) (h : algo_dom_r a b) {struct h} : bool :=
|
|
match fancy_hred a with
|
|
| inr a' => check_equal_r (proj1_sig a') b _
|
|
| inl ha' => match fancy_hred b with
|
|
| inr b' => check_equal_r a (proj1_sig b') _
|
|
| inl hb' => check_equal a b _
|
|
end
|
|
end.
|
|
|
|
Next Obligation.
|
|
simpl. intros. clear Heq_anonymous. destruct a' as [a' ha']. simpl.
|
|
inversion h; subst => //=.
|
|
exfalso. sfirstorder use:algo_dom_no_hred.
|
|
assert (a' = a'0) by eauto using hred_deter. by subst.
|
|
exfalso. sfirstorder.
|
|
Defined.
|
|
|
|
Next Obligation.
|
|
simpl. intros. clear Heq_anonymous Heq_anonymous0.
|
|
destruct b' as [b' hb']. simpl.
|
|
inversion h; subst.
|
|
- exfalso.
|
|
sfirstorder use:algo_dom_no_hred.
|
|
- exfalso.
|
|
sfirstorder.
|
|
- assert (b' = b'0) by eauto using hred_deter. by subst.
|
|
Defined.
|
|
|
|
(* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *)
|
|
Next Obligation.
|
|
move => /= a b hdom ha _ hb _.
|
|
inversion hdom; subst.
|
|
- assumption.
|
|
- exfalso; sfirstorder.
|
|
- exfalso; sfirstorder.
|
|
Defined.
|
|
|
|
Lemma check_equal_abs_abs a b h : check_equal (PAbs a) (PAbs b) (A_AbsAbs a b h) = check_equal_r a b h.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Lemma check_equal_abs_neu a u neu h : check_equal (PAbs a) u (A_AbsNeu a u neu h) = check_equal_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) h.
|
|
Proof. case : u neu h => //=. Qed.
|
|
|
|
Lemma check_equal_neu_abs a u neu h : check_equal u (PAbs a) (A_NeuAbs a u neu h) = check_equal_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a h.
|
|
Proof. case : u neu h => //=. Qed.
|
|
|
|
Lemma check_equal_pair_pair a0 b0 a1 b1 a h :
|
|
check_equal (PPair a0 b0) (PPair a1 b1) (A_PairPair a0 a1 b0 b1 a h) =
|
|
check_equal_r a0 a1 a && check_equal_r b0 b1 h.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Lemma check_equal_pair_neu a0 a1 u neu h h'
|
|
: check_equal (PPair a0 a1) u (A_PairNeu a0 a1 u neu h h') = check_equal_r a0 (PProj PL u) h && check_equal_r a1 (PProj PR u) h'.
|
|
Proof.
|
|
case : u neu h h' => //=.
|
|
Qed.
|
|
|
|
Lemma check_equal_neu_pair a0 a1 u neu h h'
|
|
: check_equal u (PPair a0 a1) (A_NeuPair a0 a1 u neu h h') = check_equal_r (PProj PL u) a0 h && check_equal_r (PProj PR u) a1 h'.
|
|
Proof.
|
|
case : u neu h h' => //=.
|
|
Qed.
|
|
|
|
Lemma check_equal_bind_bind p0 A0 B0 p1 A1 B1 h0 h1 :
|
|
check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) (A_BindCong p0 p1 A0 A1 B0 B1 h0 h1) =
|
|
BTag_eqdec p0 p1 && check_equal_r A0 A1 h0 && check_equal_r B0 B1 h1.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Lemma check_equal_proj_proj p0 u0 p1 u1 neu0 neu1 h :
|
|
check_equal (PProj p0 u0) (PProj p1 u1) (A_ProjCong p0 p1 u0 u1 neu0 neu1 h) =
|
|
PTag_eqdec p0 p1 && check_equal u0 u1 h.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Lemma check_equal_app_app u0 a0 u1 a1 hu0 hu1 hdom hdom' :
|
|
check_equal (PApp u0 a0) (PApp u1 a1) (A_AppCong u0 u1 a0 a1 hu0 hu1 hdom hdom') =
|
|
check_equal u0 u1 hdom && check_equal_r a0 a1 hdom'.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Lemma check_equal_ind_ind P0 u0 b0 c0 P1 u1 b1 c1 neu0 neu1 domP domu domb domc :
|
|
check_equal (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1)
|
|
(A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP domu domb domc) =
|
|
check_equal_r P0 P1 domP && check_equal u0 u1 domu && check_equal_r b0 b1 domb && check_equal_r c0 c1 domc.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Lemma hred_none a : HRed.nf a -> hred a = None.
|
|
Proof.
|
|
destruct (hred a) eqn:eq;
|
|
sfirstorder use:hred_complete, hred_sound.
|
|
Qed.
|
|
|
|
Ltac simp_check_r := with_strategy opaque [check_equal] simpl in *.
|
|
|
|
Lemma check_equal_nfnf a b dom : check_equal_r a b (A_NfNf a b dom) = check_equal a b dom.
|
|
Proof.
|
|
have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:algo_dom_no_hred.
|
|
have [h3 h4] : hred a = None /\ hred b = None by sfirstorder use:hf_no_hred, hne_no_hred, hred_none.
|
|
simp_check_r.
|
|
destruct (fancy_hred a).
|
|
destruct (fancy_hred b).
|
|
reflexivity.
|
|
exfalso. hauto l:on use:hred_complete.
|
|
exfalso. hauto l:on use:hred_complete.
|
|
Qed.
|
|
|
|
Lemma check_equal_hredl a b a' ha doma :
|
|
check_equal_r a b (A_HRedL a a' b ha doma) = check_equal_r a' b doma.
|
|
Proof.
|
|
simpl.
|
|
destruct (fancy_hred a).
|
|
- hauto q:on unfold:HRed.nf.
|
|
- destruct s as [x ?].
|
|
have ? : x = a' by eauto using hred_deter. subst.
|
|
simpl.
|
|
f_equal.
|
|
apply PropExtensionality.proof_irrelevance.
|
|
Qed.
|
|
|
|
Lemma check_equal_hredr a b b' hu r a0 :
|
|
check_equal_r a b (A_HRedR a b b' hu r a0) =
|
|
check_equal_r a b' a0.
|
|
Proof.
|
|
simpl.
|
|
destruct (fancy_hred a).
|
|
- simpl.
|
|
destruct (fancy_hred b) as [|[b'' hb']].
|
|
+ hauto lq:on unfold:HRed.nf.
|
|
+ simpl.
|
|
have ? : (b'' = b') by eauto using hred_deter. subst.
|
|
f_equal.
|
|
apply PropExtensionality.proof_irrelevance.
|
|
- exfalso.
|
|
sfirstorder use:hne_no_hred, hf_no_hred.
|
|
Qed.
|
|
|
|
Lemma check_equal_univ i j :
|
|
check_equal (PUniv i) (PUniv j) (A_UnivCong i j) = nat_eqdec i j.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Lemma check_equal_conf a b nfa nfb nfab :
|
|
check_equal a b (A_Conf a b nfa nfb nfab) = false.
|
|
Proof. destruct a; destruct b => //=. Qed.
|
|
|
|
#[export]Hint Rewrite check_equal_abs_abs check_equal_abs_neu check_equal_neu_abs check_equal_pair_pair check_equal_pair_neu check_equal_neu_pair check_equal_bind_bind check_equal_hredl check_equal_hredr check_equal_nfnf check_equal_conf : ce_prop.
|
|
|
|
Ltac2 destruct_salgo () :=
|
|
lazy_match! goal with
|
|
| [h : salgo_dom ?a ?b |- _ ] =>
|
|
if is_var a then destruct $a; ltac1:(done) else
|
|
(if is_var b then destruct $b; ltac1:(done) else ())
|
|
end.
|
|
|
|
Ltac check_sub_triv :=
|
|
intros;subst;
|
|
lazymatch goal with
|
|
(* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *)
|
|
| [_ : salgo_dom _ _ |- _] => try (inversion h; subst => //=; ltac2:(Control.enter destruct_algo))
|
|
| _ => idtac
|
|
end.
|
|
|
|
Local Obligation Tactic := try solve [check_sub_triv | sfirstorder].
|
|
|
|
Program Fixpoint check_sub (a b : PTm) (h : salgo_dom a b) {struct h} :=
|
|
match a, b with
|
|
| PBind PPi A0 B0, PBind PPi A1 B1 =>
|
|
check_sub_r A1 A0 _ && check_sub_r B0 B1 _
|
|
| PBind PSig A0 B0, PBind PSig A1 B1 =>
|
|
check_sub_r A0 A1 _ && check_sub_r B0 B1 _
|
|
| PUniv i, PUniv j =>
|
|
PeanoNat.Nat.leb i j
|
|
| PNat, PNat => true
|
|
| PApp _ _ , PApp _ _ => check_equal a b _
|
|
| VarPTm _, VarPTm _ => check_equal a b _
|
|
| PInd _ _ _ _, PInd _ _ _ _ => check_equal a b _
|
|
| PProj _ _, PProj _ _ => check_equal a b _
|
|
| _, _ => false
|
|
end
|
|
with check_sub_r (a b : PTm) (h : salgo_dom_r a b) {struct h} :=
|
|
match fancy_hred a with
|
|
| inr a' => check_sub_r (proj1_sig a') b _
|
|
| inl ha' => match fancy_hred b with
|
|
| inr b' => check_sub_r a (proj1_sig b') _
|
|
| inl hb' => check_sub a b _
|
|
end
|
|
end.
|
|
|
|
Next Obligation.
|
|
simpl. intros. clear Heq_anonymous. destruct a' as [a' ha']. simpl.
|
|
inversion h; subst => //=.
|
|
exfalso. sfirstorder use:salgo_dom_no_hred.
|
|
assert (a' = a'0) by eauto using hred_deter. by subst.
|
|
exfalso. sfirstorder.
|
|
Defined.
|
|
|
|
Next Obligation.
|
|
simpl. intros. clear Heq_anonymous Heq_anonymous0.
|
|
destruct b' as [b' hb']. simpl.
|
|
inversion h; subst.
|
|
- exfalso.
|
|
sfirstorder use:salgo_dom_no_hred.
|
|
- exfalso.
|
|
sfirstorder.
|
|
- assert (b' = b'0) by eauto using hred_deter. by subst.
|
|
Defined.
|
|
|
|
(* Need to avoid ssreflect tactics since they generate terms that make the termination checker upset *)
|
|
Next Obligation.
|
|
move => /= a b hdom ha _ hb _.
|
|
inversion hdom; subst.
|
|
- assumption.
|
|
- exfalso; sfirstorder.
|
|
- exfalso; sfirstorder.
|
|
Defined.
|
|
|
|
Lemma check_sub_pi_pi A0 B0 A1 B1 h0 h1 :
|
|
check_sub (PBind PPi A0 B0) (PBind PPi A1 B1) (S_PiCong A0 A1 B0 B1 h0 h1) =
|
|
check_sub_r A1 A0 h0 && check_sub_r B0 B1 h1.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Lemma check_sub_sig_sig A0 B0 A1 B1 h0 h1 :
|
|
check_sub (PBind PSig A0 B0) (PBind PSig A1 B1) (S_SigCong A0 A1 B0 B1 h0 h1) =
|
|
check_sub_r A0 A1 h0 && check_sub_r B0 B1 h1.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Lemma check_sub_univ_univ i j :
|
|
check_sub (PUniv i) (PUniv j) (S_UnivCong i j) = PeanoNat.Nat.leb i j.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Lemma check_sub_nfnf a b dom : check_sub_r a b (S_NfNf a b dom) = check_sub a b dom.
|
|
Proof.
|
|
have [h0 h1] : HRed.nf a /\ HRed.nf b by hauto l:on use:salgo_dom_no_hred.
|
|
have [h3 h4] : hred a = None /\ hred b = None by sfirstorder use:hf_no_hred, hne_no_hred, hred_none.
|
|
simpl.
|
|
destruct (fancy_hred b)=>//=.
|
|
destruct (fancy_hred a) =>//=.
|
|
destruct s as [a' ha']. simpl.
|
|
hauto l:on use:hred_complete.
|
|
destruct s as [b' hb']. simpl.
|
|
hauto l:on use:hred_complete.
|
|
Qed.
|
|
|
|
Lemma check_sub_hredl a b a' ha doma :
|
|
check_sub_r a b (S_HRedL a a' b ha doma) = check_sub_r a' b doma.
|
|
Proof.
|
|
simpl.
|
|
destruct (fancy_hred a).
|
|
- hauto q:on unfold:HRed.nf.
|
|
- destruct s as [x ?].
|
|
have ? : x = a' by eauto using hred_deter. subst.
|
|
simpl.
|
|
f_equal.
|
|
apply PropExtensionality.proof_irrelevance.
|
|
Qed.
|
|
|
|
Lemma check_sub_hredr a b b' hu r a0 :
|
|
check_sub_r a b (S_HRedR a b b' hu r a0) =
|
|
check_sub_r a b' a0.
|
|
Proof.
|
|
simpl.
|
|
destruct (fancy_hred a).
|
|
- simpl.
|
|
destruct (fancy_hred b) as [|[b'' hb']].
|
|
+ hauto lq:on unfold:HRed.nf.
|
|
+ simpl.
|
|
have ? : (b'' = b') by eauto using hred_deter. subst.
|
|
f_equal.
|
|
apply PropExtensionality.proof_irrelevance.
|
|
- exfalso.
|
|
sfirstorder use:hne_no_hred, hf_no_hred.
|
|
Qed.
|
|
|
|
Lemma check_sub_neuneu a b i a0 : check_sub a b (S_NeuNeu a b i a0) = check_equal a b a0.
|
|
Proof. destruct a,b => //=. Qed.
|
|
|
|
Lemma check_sub_conf a b n n0 i : check_sub a b (S_Conf a b n n0 i) = false.
|
|
Proof. destruct a,b=>//=; ecrush inv:BTag. Qed.
|
|
|
|
#[export]Hint Rewrite check_sub_neuneu check_sub_conf check_sub_hredl check_sub_hredr check_sub_nfnf check_sub_univ_univ check_sub_pi_pi check_sub_sig_sig : ce_prop.
|