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

Make progress on the completeness proof

Browse source
This commit is contained in:
Yiyun Liu 2025-02-27 00:07:57 -05:00
parent af0cac15e6
commit aaec928902
1 changed files with 32 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

35
theories/algorithmic.v
View file

@ -1227,7 +1227,14 @@ Lemma algo_metric_suc n k (a0 a1 : PTm n) :
Proof. Proof.
move => [i][j][va][vb][h0][h1][h2][h3][h4]h5. move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
exists (k - 1). exists (k - 1).
move /lored_nsteps_suc_inv : h0.
move => [a0'][ha0]?. subst.
move /lored_nsteps_suc_inv : h1.
move => [b0'][hb0]?. subst. simpl in *.
split; first by lia.
rewrite /algo_metric.
hauto lq:on rew:off use:EJoin.suc_inj solve+:lia.
Qed.
Lemma algo_metric_bind n k p0 (A0 : PTm n) B0 p1 A1 B1 : Lemma algo_metric_bind n k p0 (A0 : PTm n) B0 p1 A1 B1 :
algo_metric k (PBind p0 A0 B0) (PBind p1 A1 B1) -> algo_metric k (PBind p0 A0 B0) (PBind p1 A1 B1) ->
@ -1430,6 +1437,13 @@ Proof.
* move => > /algo_metric_join. * move => > /algo_metric_join.
hauto lq:on rew:off use:REReds.suc_inv, REReds.zero_inv. hauto lq:on rew:off use:REReds.suc_inv, REReds.zero_inv.
* move => a0 a1 h _ _. * move => a0 a1 h _ _.
move /algo_metric_suc : h => [j [h4 h5]].
move => Γ A /Suc_Inv [h0 h1] /Suc_Inv [h2 h3].
move : ih h4 h5;do!move/[apply].
move => [ih _].
move : ih h0 h2;do!move/[apply].
move => h. apply : CE_HRed; eauto using rtc_refl.
by constructor.
- move : k a b h fb fa. abstract : hnfneu. - move : k a b h fb fa. abstract : hnfneu.
move => k. move => k.
move => + b. move => + b.
@ -1488,9 +1502,24 @@ Proof.
+ hauto lq:on rew:off use:DJoin.hne_univ_noconf, algo_metric_join. + hauto lq:on rew:off use:DJoin.hne_univ_noconf, algo_metric_join.
+ hauto lq:on rew:off use:DJoin.hne_nat_noconf, algo_metric_join. + hauto lq:on rew:off use:DJoin.hne_nat_noconf, algo_metric_join.
(* Zero *) (* Zero *)
+ admit. + case => //=.
* move => i /algo_metric_join. clear.
hauto lq:on rew:off use:REReds.var_inv, REReds.zero_inv.
* move => >/algo_metric_join. clear.
hauto lq:on rew:off use:REReds.hne_app_inv, REReds.zero_inv.
* move => >/algo_metric_join. clear.
hauto lq:on rew:off use:REReds.hne_proj_inv, REReds.zero_inv.
* sfirstorder use:T_Bot_Imp.
* move => >/algo_metric_join. clear.
move => h _ h2. exfalso.
hauto q:on use:REReds.hne_ind_inv, REReds.zero_inv.
(* Suc *) (* Suc *)
+ admit. + move => a0.
case => //=; move => >/algo_metric_join; clear.
* hauto lq:on rew:off use:REReds.var_inv, REReds.suc_inv.
* hauto lq:on rew:off use:REReds.hne_app_inv, REReds.suc_inv.
* hauto lq:on rew:off use:REReds.hne_proj_inv, REReds.suc_inv.
*
- move {ih}. - move {ih}.
move /algo_metric_sym in h. move /algo_metric_sym in h.
qauto l:on use:coqeq_symmetric_mutual. qauto l:on use:coqeq_symmetric_mutual.