pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising before class

Browse source
This commit is contained in:
Adam Chlipala 2020-04-26 14:29:53 -04:00
parent 213f8b270b
commit 42d5af6d2d
1 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
ProgramDerivation_template.v
View file

@ -2,6 +2,8 @@ Require Import Frap.
Require Import Program Setoids.Setoid Classes.RelationClasses Classes.Morphisms Morphisms_Prop. Require Import Program Setoids.Setoid Classes.RelationClasses Classes.Morphisms Morphisms_Prop.
Require Import Eqdep. Require Import Eqdep.
Set Warnings "-cannot-define-projection".
Ltac inv_pair := Ltac inv_pair :=
match goal with match goal with
| [ H : existT _ _ _ = existT _ _ _ |- _ ] => apply inj_pair2 in H; invert H | [ H : existT _ _ _ = existT _ _ _ |- _ ] => apply inj_pair2 in H; invert H
@ -185,7 +187,7 @@ Inductive RefineMethods {state1 state2} (R : state1 -> state2 -> Prop)
-> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1) -> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1)
(MethodsCons {| MethodName := name; MethodBody := f2 |} ms2). (MethodsCons {| MethodName := name; MethodBody := f2 |} ms2).
Hint Constructors RefineMethods. Hint Constructors RefineMethods : core.
Record adt_refine {names} (adt1 adt2 : adt names) : Prop := { Record adt_refine {names} (adt1 adt2 : adt names) : Prop := {
ArRel : AdtState adt1 -> AdtState adt2 -> Prop; ArRel : AdtState adt1 -> AdtState adt2 -> Prop;
@ -212,7 +214,7 @@ Definition split_counter := ADT {
and method "value"[[self, _]] = ret (self, fst self + snd self) and method "value"[[self, _]] = ret (self, fst self + snd self)
}. }.
Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic. Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic : core.
Theorem split_counter_ok : adt_refine counter split_counter. Theorem split_counter_ok : adt_refine counter split_counter.
Proof. Proof.
@ -230,7 +232,7 @@ Proof.
subst; eauto. subst; eauto.
Qed. Qed.
Hint Immediate RefineMethods_refl. Hint Immediate RefineMethods_refl : core.
Theorem refine_refl : forall names (adt1 : adt names), Theorem refine_refl : forall names (adt1 : adt names),
adt_refine adt1 adt1. adt_refine adt1 adt1.
@ -259,7 +261,7 @@ Proof.
first_order. first_order.
Qed. Qed.
Hint Resolve RefineMethods_trans. Hint Resolve RefineMethods_trans : core.
Theorem refine_trans : forall names (adt1 adt2 adt3 : adt names), Theorem refine_trans : forall names (adt1 adt2 adt3 : adt names),
adt_refine adt1 adt2 adt_refine adt1 adt2
@ -322,7 +324,7 @@ Proof.
simplify; subst; eauto. simplify; subst; eauto.
Qed. Qed.
Hint Resolve ReplaceMethod_ok. Hint Resolve ReplaceMethod_ok : core.
Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat)) Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat))
names (ms1 ms2 : methods state names) constr, names (ms1 ms2 : methods state names) constr,
@ -367,7 +369,7 @@ Proof.
eauto. eauto.
Qed. Qed.
Hint Resolve RepChangeMethods_ok. Hint Resolve RepChangeMethods_ok : core.
Theorem refine_rep : forall state1 state2 (absfunc : state2 -> state1) Theorem refine_rep : forall state1 state2 (absfunc : state2 -> state1)
names (ms1 : methods state1 names) (ms2 : methods state2 names) names (ms1 : methods state1 names) (ms2 : methods state2 names)
@ -424,7 +426,7 @@ Inductive CachingMethods {state} (name : string) (func : state -> nat)
CachingMethods name func ms1 ms2 CachingMethods name func ms1 ms2
-> CachingMethods name func -> CachingMethods name func
(MethodsCons {| MethodName := name; MethodBody := (fun s _ => ret (s, func s)) |} ms1) (MethodsCons {| MethodName := name; MethodBody := (fun s _ => ret (s, func s)) |} ms1)
(MethodsCons {| MethodName := name; MethodBody := (fun s arg => ret (s, snd s)) |} ms2) (MethodsCons {| MethodName := name; MethodBody := (fun s _ => ret (s, snd s)) |} ms2)
| CmDefault : forall name' names oldbody (ms1 : methods state names) (ms2 : methods _ names), | CmDefault : forall name' names oldbody (ms1 : methods state names) (ms2 : methods _ names),
name' <> name name' <> name
-> CachingMethods name func ms1 ms2 -> CachingMethods name func ms1 ms2
@ -458,7 +460,7 @@ Proof.
eauto. eauto.
Qed. Qed.
Hint Resolve CachingMethods_ok. Hint Resolve CachingMethods_ok : core.
Theorem refine_cache : forall state name (func : state -> nat) Theorem refine_cache : forall state name (func : state -> nat)
names (ms1 : methods state names) (ms2 : methods (state * nat) names) names (ms1 : methods state names) (ms2 : methods (state * nat) names)