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

Add stubs for lemmas needed for completeness

Browse source
This commit is contained in:
Yiyun Liu 2025-02-16 01:22:15 -05:00
parent 0f48a485be
commit 06d420aa7e
1 changed files with 18 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

18
theories/algorithmic.v
View file

@ -558,6 +558,7 @@ Proof.
- sfirstorder use:ne_hne. - sfirstorder use:ne_hne.
- hauto lq:on ctrs:HRed.R. - hauto lq:on ctrs:HRed.R.
Qed. Qed.
Lemma algo_metric_case n k (a b : PTm n) : Lemma algo_metric_case n k (a b : PTm n) :
algo_metric k a b -> algo_metric k a b ->
(ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ algo_metric k' a' b /\ k' < k. (ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ algo_metric k' a' b /\ k' < k.
@ -770,6 +771,23 @@ Proof.
lia. lia.
Qed. Qed.
Lemma algo_metric_pair n k (a0 b0 a1 b1 : PTm n) :
SN (PPair a0 b0) ->
SN (PPair a1 b1) ->
algo_metric k (PPair a0 b0) (PPair a1 b1) ->
exists j, j < k /\ algo_metric j a0 a1 /\ algo_metric j b0 b1.
Admitted.
Lemma algo_metric_neu_abs n k (a0 : PTm (S n)) u :
algo_metric k u (PAbs a0) ->
exists j, j < k /\ algo_metric j (PApp (ren_PTm shift u) (VarPTm var_zero)) a0.
Admitted.
Lemma algo_metric_neu_pair n k (a0 b0 : PTm n) u :
algo_metric k u (PPair a0 b0) ->
exists j, j < k /\ algo_metric j (PProj PL u) a0 /\ algo_metric j (PProj PR u) b0.
Admitted.
Lemma algo_metric_app n k (a0 b0 a1 b1 : PTm n) : Lemma algo_metric_app n k (a0 b0 a1 b1 : PTm n) :
algo_metric k (PApp a0 b0) (PApp a1 b1) -> algo_metric k (PApp a0 b0) (PApp a1 b1) ->
ishne a0 -> ishne a0 ->