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

Prove termination

Browse source
This commit is contained in:
Yiyun Liu 2025-03-06 15:39:27 -05:00
parent b29d567ef0
commit 96b3139726
4 changed files with 266 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

13
theories/executable_correct.v
View file

@ -4,12 +4,6 @@ Require Import ssreflect ssrbool.
From stdpp Require Import relations (rtc(..)).
From Hammer Require Import Tactics.
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 coqeqr_no_hred a b : a ∼ b -> HRed.nf a /\ HRed.nf b.
Proof. induction 1; sauto lq:on unfold:HRed.nf. Qed.
@ -18,7 +12,6 @@ Proof. induction 1;
qauto inv:HRed.R use:coqeqr_no_hred, hne_no_hred unfold:HRed.nf.
Qed.
Lemma coqeq_neuneu u0 u1 :
ishne u0 -> ishne u1 -> u0 ↔ u1 -> u0 ∼ u1.
Proof.
@ -88,12 +81,6 @@ Proof.
sauto lq:on rew:off.
Qed.
Lemma hreds_nf_refl a b :
HRed.nf a ->
rtc HRed.R a b ->
a = b.
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 :