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

Add stub for check_sub

Browse source
This commit is contained in:
Yiyun Liu 2025-03-06 16:20:32 -05:00
parent 96b3139726
commit 6f154cc9c6
2 changed files with 34 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

22
theories/executable.v
View file

@ -212,6 +212,11 @@ with algo_dom_r : PTm -> PTm -> Prop :=
(* ----------------------- *) (* ----------------------- *)
algo_dom_r a b. algo_dom_r a b.
Scheme algo_ind := Induction for algo_dom Sort Prop
with algor_ind := Induction for algo_dom_r Sort Prop.
Combined Scheme algo_dom_mutual from algo_ind, algor_ind.
Lemma hf_no_hred (a b : PTm) : Lemma hf_no_hred (a b : PTm) :
ishf a -> ishf a ->
HRed.R a b -> HRed.R a b ->
@ -351,7 +356,6 @@ Ltac solve_check_equal :=
| inr b' := check_equal_r a (proj1_sig b') _; | inr b' := check_equal_r a (proj1_sig b') _;
| inl h'' := check_equal a b _. | inl h'' := check_equal a b _.
Next Obligation. Next Obligation.
intros. intros.
inversion h; subst => //=. inversion h; subst => //=.
@ -487,7 +491,17 @@ 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. #[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.
Scheme algo_ind := Induction for algo_dom Sort Prop Obligation Tactic := solve [check_equal_triv | sfirstorder].
with algor_ind := Induction for algo_dom_r Sort Prop.
Combined Scheme algo_dom_mutual from algo_ind, algor_ind. Program Fixpoint check_sub (q : bool) (a b : PTm) (h : algo_dom a b) {struct h} :=
match a, b with
| PBind PPi A0 B0, PBind PPi A1 B1 =>
check_sub_r (negb q) A0 A1 _ && check_sub_r q B0 B1 _
| PBind PSig A0 B0, PBind PSig A1 B1 =>
check_sub_r q A0 A1 _ && check_sub_r q B0 B1 _
| PUniv i, PUniv j =>
if q then PeanoNat.Nat.leb i j else PeanoNat.Nat.leb j i
| PNat, PNat => true
| _ ,_ => ishne a && ishne b && check_equal a b h
end
with check_sub_r (q : bool) (a b : PTm) (h : algo_dom_r a b) {struct h} := false.

16
theories/termination.v
View file

@ -264,3 +264,19 @@ Proof.
have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred. have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred.
hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom. hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom.
Qed. Qed.
Lemma sn_term_metric (a b : PTm) : SN a -> SN b -> exists k, term_metric k a b.
Proof.
move /LoReds.FromSN => [va [ha0 ha1]].
move /LoReds.FromSN => [vb [hb0 hb1]].
eapply relations.rtc_nsteps in ha0.
eapply relations.rtc_nsteps in hb0.
hauto lq:on unfold:term_metric solve+:lia.
Qed.
Lemma sn_algo_dom a b : SN a -> SN b -> algo_dom_r a b.
Proof.
move : sn_term_metric; repeat move/[apply].
move => [k]+.
eauto using term_metric_algo_dom.
Qed.