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

Add standardization_lo

Browse source
This commit is contained in:
Yiyun Liu 2025-02-16 23:00:23 -05:00
parent bdba6f50e5
commit 21d9a2ce1b
2 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
theories/algorithmic.v
View file

@ -875,7 +875,10 @@ Qed.
Lemma algo_metric_neu_pair n k (a0 b0 : PTm n) u :
algo_metric k u (PPair a0 b0) ->
ishne u ->
exists j, j < k /\ algo_metric j (PProj PL u) a0 /\ algo_metric j (PProj PR u) b0.
Proof.
move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 neu.
Admitted.
Lemma algo_metric_app n k (a0 b0 a1 b1 : PTm n) :

14
theories/fp_red.v
View file

@ -2515,6 +2515,20 @@ Module DJoin.
hauto q:on use:NeEPars.ToEReds unfold:EJoin.R.
Qed.
Lemma standardization_lo n (a b : PTm n) :
SN a -> SN b -> R a b ->
exists va vb, rtc LoRed.R a va /\ rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb.
Proof.
move => /[dup] sna + /[dup] snb.
move : standardization; repeat move/[apply].
move => [va][vb][hva][hvb][nfva][nfvb]hj.
move /LoReds.FromSN : sna => [va' [hva' hva'0]].
move /LoReds.FromSN : snb => [vb' [hvb' hvb'0]].
exists va', vb'.
repeat split => //=.
have : va = va' /\ vb = vb' by sfirstorder use:red_uniquenf, LoReds.ToRReds.
case; congruence.
Qed.
End DJoin.