| Some example programs and proofs of their correctness |
Require Import List.
Require Import Binding.
Require Import PSLC.
Require Import MemMonad.
Require Import Imp.
Set Implicit Arguments.
Source language |
| A specialization of the denotation function to closed terms |
Definition meaning (t : ty) (e : term nil t) : tyDenote t :=
termDenote e (SNil _).
Definition snd : term nil (Arrow (Data Nat) (Arrow (Data Nat) (Data Nat))) :=
Lam (Lam (EVar (First _ _))).
Theorem snd_ok : forall n1 n2,
meaning (App (App snd (Const _ n1)) (Const _ n2))
= meaning (Const _ n2).
trivial.
Qed.
| That was easy! This theorem is actually proved by reflexivity with a single proof constructor, since Coq identifies terms up to computational reduction. |
Definition dup : term nil (Arrow (Data Nat) (Data (Prod Nat Nat))) :=
Lam (Pair (EVar (First _ _)) (EVar (First _ _))).
Theorem dup_ok : forall n,
meaning (Fst (App dup (Const _ n)))
= meaning (Const _ n).
trivial.
Qed.
| Another trivial one. |
Definition JM_case : term nil (Arrow (Data (Sum Nat Nat)) (Data Nat)) :=
Lam (Case (EVar (First _ _))
(Const _ 42)
(Const _ 42)).
Theorem JM_case_ok : forall (e : term nil (Data (Sum Nat Nat))),
meaning (App JM_case e)
= meaning (Const _ 42).
unfold meaning; simplify;
destruct (termDenote e (SNil _)); trivial.
Qed.
This one was a little more work, but not much.
Definitional equality wasn't strong enough to prove the goal, but asking
explicitly for a case analysis over the denotation of the argument e was
enough.
|
Target language |
Definition imeaning (t : ity) (e : iterm nil t) : ityDenote t :=
itermDenote e (SNil _).
Our generic strategy for proving term correctness:
Expand the definition of our specialized denotation function for closed terms
and then ask the MemMonad library to work its magic.
|
Ltac simp := unfold imeaning; memM_simplify.
Definition read_back : iterm nil (IArrow (IData INat) (IData INat)) :=
ILam (ISeq
(IWrite (IConst _ O) (IVar (First _ _)))
(IRead (IConst _ O))).
Theorem read_back_ok : forall m n,
mspec (fun _ n' => n' = n) (imeaning (IApp read_back (IConst _ n))) m.
simp.
Qed.
Here, the actual proof term generated (you can see it with memM_simplify tactic does the
work for us.
|
Definition scribbler : iterm nil (IArrow (IData INat) (IData INat)) :=
ILam (ISeq
(IWrite (IVar (First _ _)) (IConst _ 0))
(ISeq
(IWrite (ISucc (IVar (First _ _))) (IConst _ 1))
(IRead (IVar (First _ _))))).
Theorem scribbler_ok : forall m a,
mspec (fun _ n => n = O) (imeaning (IApp scribbler (IConst _ a))) m.
simp.
Qed.
Another victory for memM_simplify
|