Commit d8ad2335 authored by Ralf Jung's avatar Ralf Jung

group definitions better

parent 31321366
......@@ -68,6 +68,11 @@ Module LiftingTests.
n1.
Definition FindPred n2 := Rec (Let (Plus (Var 1) (LitNat 1))
(FindPred' (Var 2) (Var 0) n2.[ren(+3)] (Var 1))).
Definition Pred := Lam (If (Le (Var 0) (LitNat 0))
(LitNat 0)
(App (FindPred (Var 0)) (LitNat 0))
).
Lemma FindPred_spec n1 n2 E Q :
((n1 < n2) Q (LitNatV $ pred n2))
wp (Σ:=Σ) E (App (FindPred (LitNat n2)) (LitNat n1)) Q.
......@@ -97,10 +102,6 @@ Module LiftingTests.
assert (Heq: n1 = pred n2) by omega. by subst n1.
Qed.
Definition Pred := Lam (If (Le (Var 0) (LitNat 0))
(LitNat 0)
(App (FindPred (Var 0)) (LitNat 0))
).
Lemma Pred_spec n E Q :
Q (LitNatV $ pred n) wp (Σ:=Σ) E (App Pred (LitNat n)) Q.
Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment