yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update the correctness proof of the computable function

Browse source
This commit is contained in:
Yiyun Liu 2025-03-04 23:48:42 -05:00
parent c1ff0ae145
commit c4f01d7dfc
2 changed files with 29 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

4
theories/executable.v
View file

@ -477,6 +477,10 @@ Proof.
sfirstorder use:hne_no_hred, hf_no_hred. sfirstorder use:hne_no_hred, hf_no_hred.
Qed. 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 : Lemma check_equal_conf a b nfa nfb nfab :
check_equal a b (A_Conf a b nfa nfb nfab) = false. check_equal a b (A_Conf a b nfa nfb nfab) = false.
Proof. destruct a; destruct b => //=. Qed. Proof. destruct a; destruct b => //=. Qed.

44
theories/executable_correct.v
View file

@ -37,8 +37,7 @@ Proof.
- move => a u i h0 ih h. - move => a u i h0 ih h.
apply CE_AbsNeu => //. apply CE_AbsNeu => //.
apply : ih. simp check_equal tm_to_eq_view in h. apply : ih. simp check_equal tm_to_eq_view in h.
have h1 : check_equal (PAbs a) u (A_AbsNeu a u i h0) = check_equal_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) h0 by clear; case : u i h0 => //=. by rewrite check_equal_abs_neu in h.
hauto lq:on.
- move => a u i h ih h0. - move => a u i h ih h0.
apply CE_NeuAbs=>//. apply CE_NeuAbs=>//.
apply ih. apply ih.
@ -79,6 +78,7 @@ Proof.
rewrite check_equal_ind_ind. rewrite check_equal_ind_ind.
move /andP => [/andP [/andP [h0 h1] h2 ] h3]. move /andP => [/andP [/andP [h0 h1] h2 ] h3].
sauto lq:on use:coqeq_neuneu. sauto lq:on use:coqeq_neuneu.
- move => a b n n0 i. by rewrite check_equal_conf.
- move => a b dom h ih. apply : CE_HRed; eauto using rtc_refl. - move => a b dom h ih. apply : CE_HRed; eauto using rtc_refl.
rewrite check_equal_nfnf in ih. rewrite check_equal_nfnf in ih.
tauto. tauto.
@ -94,27 +94,25 @@ Lemma hreds_nf_refl a b :
a = b. a = b.
Proof. inversion 2; sfirstorder. Qed. Proof. inversion 2; sfirstorder. Qed.
Ltac ce_solv := move => *; simp ce_prop in *; hauto qb:on rew:off inv:CoqEq, CoqEq_Neu.
Lemma check_equal_complete : Lemma check_equal_complete :
(forall a b (h : algo_dom a b), ~ check_equal a b h -> ~ a ↔ b) /\ (forall a b (h : algo_dom a b), ~ check_equal a b h -> ~ a ↔ b) /\
(forall a b (h : algo_dom_r a b), ~ check_equal_r a b h -> ~ a ⇔ b). (forall a b (h : algo_dom_r a b), ~ check_equal_r a b h -> ~ a ⇔ b).
Proof. Proof.
apply algo_dom_mutual. apply algo_dom_mutual.
- hauto q:on inv:CoqEq, CoqEq_Neu b:on rew:db:ce_prop. - ce_solv.
- hauto q:on inv:CoqEq, CoqEq_Neu b:on rew:db:ce_prop. - ce_solv.
- hauto q:on inv:CoqEq, CoqEq_Neu b:on rew:db:ce_prop. - ce_solv.
- hauto q:on inv:CoqEq, CoqEq_Neu b:on rew:db:ce_prop. - ce_solv.
- hauto q:on inv:CoqEq, CoqEq_Neu b:on rew:db:ce_prop. - ce_solv.
- hauto q:on inv:CoqEq, CoqEq_Neu b:on rew:db:ce_prop. - ce_solv.
- hauto q:on inv:CoqEq, CoqEq_Neu b:on rew:db:ce_prop. - ce_solv.
- hauto q:on inv:CoqEq, CoqEq_Neu b:on rew:db:ce_prop. - ce_solv.
- move => i j. - move => i j.
move => h0 h1. rewrite check_equal_univ.
have ? : i = j by sauto lq:on. subst. case : nat_eqdec => //=.
simp check_equal in h0. ce_solv.
set x := (nat_eqdec j j).
destruct x as [].
sauto q:on.
sfirstorder.
- move => p0 p1 A0 A1 B0 B1 h0 ih0 h1 ih1. - move => p0 p1 A0 A1 B0 B1 h0 ih0 h1 ih1.
rewrite check_equal_bind_bind. rewrite check_equal_bind_bind.
move /negP. move /negP.
@ -125,8 +123,8 @@ Proof.
hauto qb:on inv:CoqEq,CoqEq_Neu. hauto qb:on inv:CoqEq,CoqEq_Neu.
hauto qb:on inv:CoqEq,CoqEq_Neu. hauto qb:on inv:CoqEq,CoqEq_Neu.
- simp check_equal. done. - simp check_equal. done.
- move => i j. simp check_equal. - move => i j. move => h. have {h} : ~ nat_eqdec i j by done.
case : nat_eqdec => //=. sauto lq:on. case : nat_eqdec => //=. ce_solv.
- move => p0 p1 u0 u1 neu0 neu1 h ih. - move => p0 p1 u0 u1 neu0 neu1 h ih.
rewrite check_equal_proj_proj. rewrite check_equal_proj_proj.
move /negP /nandP. case. move /negP /nandP. case.
@ -147,6 +145,14 @@ Proof.
sauto lqb:on inv:CoqEq, CoqEq_Neu. sauto lqb:on inv:CoqEq, CoqEq_Neu.
sauto lqb:on inv:CoqEq, CoqEq_Neu. sauto lqb:on inv:CoqEq, CoqEq_Neu.
sauto lqb:on inv:CoqEq, CoqEq_Neu. sauto lqb:on inv:CoqEq, CoqEq_Neu.
- rewrite /tm_conf.
move => a b n n0 i. simp ce_prop.
move => _. inversion 1; subst => //=.
+ destruct b => //=.
+ destruct a => //=.
+ destruct b => //=.
+ destruct a => //=.
+ hauto l:on inv:CoqEq_Neu.
- move => a b h ih. - move => a b h ih.
rewrite check_equal_nfnf. rewrite check_equal_nfnf.
move : ih => /[apply]. move : ih => /[apply].