From 210c27a7a8b6365bbede2e91b8707c8393049e65 Mon Sep 17 00:00:00 2001 From: "brandon.3.moore" Date: Fri, 18 Oct 2013 19:32:13 +0000 Subject: [PATCH] Use more semantic style of coinduction --- coq/playground/himp/Makefile | 4 +- coq/playground/himp/README | 59 ++++ coq/playground/himp/coinduction.v | 52 +++ coq/playground/himp/domains.v | 3 + coq/playground/himp/equate_map_reflection.v | 308 +++++++++++++++++ coq/playground/himp/eval_proofs.v | 110 ++++++ coq/playground/himp/kstep.v | 133 +++++++ coq/playground/himp/kstyle.v | 364 ++------------------ coq/playground/himp/mult_proof.v | 97 ++++++ coq/playground/himp/simple_proofs.v | 274 ++++++++------- 10 files changed, 935 insertions(+), 469 deletions(-) create mode 100644 coq/playground/himp/README create mode 100644 coq/playground/himp/coinduction.v create mode 100644 coq/playground/himp/equate_map_reflection.v create mode 100644 coq/playground/himp/eval_proofs.v create mode 100644 coq/playground/himp/kstep.v create mode 100644 coq/playground/himp/mult_proof.v diff --git a/coq/playground/himp/Makefile b/coq/playground/himp/Makefile index 713e5c6..eff295c 100644 --- a/coq/playground/himp/Makefile +++ b/coq/playground/himp/Makefile @@ -10,10 +10,10 @@ extractclean : rm -f extraction.vo extraction.glob extraction.v.d .PHONY : all extract clean extractclean distclean -FILES=domains.v kstyle.v evaluator.v simple_proofs.v equate_map_reflection.v +FILES=domains.v kstep.v kstyle.v coinduction.v simple_proofs.v equate_map_reflection.v evaluator.v eval_proofs.v coq_makefile.mk : Makefile - coq_makefile ${FILES} -install none -o tmp.mk -R ../../ml_proof '' && mv tmp.mk $@ + coq_makefile ${FILES} -install none -o tmp.mk && mv tmp.mk $@ eval.ml eval.mli : evaluator.vo extraction.v kstyle.vo coqc extraction.v diff --git a/coq/playground/himp/README b/coq/playground/himp/README new file mode 100644 index 0000000..53d903c --- /dev/null +++ b/coq/playground/himp/README @@ -0,0 +1,59 @@ +Organization: + +Basic definition of the language: + +domains.v defines maps and the syntx of terms. +Maps are defined by empty, item, and join constructors, +equipped with a suitable equivalence relation and +tactics for reordering maps to make lookups go through. + +kstep.v defines just the step relation, it's split +into a separate file because the Inductive relation +definition is too big to step past in Proof General +(an emacs bug limiting the size of buffers that can +be sent to external processes). + +kstyle.v completes the definition of the language, +by defining an equivalence relation on configurations, +and showing that the step relation takes related +configurations to related configurations. + +coinduction.v defines the reachability relation, +and a system of derived rules for proving +reachability properties, and some tactics +for automatically evaluating with them. + +simple_proofs.v +Some basic proofs for developing the proof automation tactics. + +**mult_proof.v +Prove a multiply function, using transitivity and a set of circularities +(incompletely extracted, not in Makefile) +**reverse.v +Prove a linked-list reverse function. +(incompletely extracted, not in Makefile) + +Evaluation function: + +evaluator.v +defines an evaluation as a function and proves it's +faithful to the step function. + +eval_proofs.v +Testing use of the evaluation function in Coq, +and speed of reducing applications of it in various ways. + +extraction.v +contains commands to extract an executable OCaml function +from the evaluator. + +run.ml +is a tiny little O'Caml driver that applies the extracted +step function to a program until it finishes, or forever +(can't be written in Coq because it's not total) + +Experimental: + +equate_map_reflection.v +trying to replace the map-aligning tactics with +proof by reflection. diff --git a/coq/playground/himp/coinduction.v b/coq/playground/himp/coinduction.v new file mode 100644 index 0000000..4755d2c --- /dev/null +++ b/coq/playground/himp/coinduction.v @@ -0,0 +1,52 @@ +Set Implicit Arguments. + +Require Import domains. +Require Import kstyle. + +CoInductive reaches (x : kcfg) (P : kcfg -> Prop) : Prop := + | done : P x -> reaches x P + | step : forall y, kstep x y -> reaches y P -> reaches x P + . + +Definition steps x y := reaches x (kequiv y). + +Definition RRel : Type := kcfg -> (kcfg -> Prop) -> Prop. +Definition subrel (kcfg B : RRel) : Prop := forall x P, kcfg x P -> B x P. + +Definition sound (X : RRel) : Prop := subrel X reaches. + +(* Base functor of the path predicate *) +Inductive stepF (X : RRel) (x : kcfg) (P : kcfg -> Prop) : Prop := + | DoneF : P x -> stepF X x P + | StepF : forall y, kstep x y -> X y P -> stepF X x P. + +Definition stable (X : RRel) : Prop := subrel X (stepF X). + +CoFixpoint stable_sound X (Hstable : stable X) : sound X := + fun x P HxP => + match Hstable _ _ HxP with + | DoneF Px => done _ _ Px + | StepF y Rxy XyP => step Rxy (@stable_sound _ Hstable _ _ XyP) + end. + +Definition F_stable (F : RRel -> RRel) (X : RRel) : Prop := subrel X (stepF (F X)). + +(* Direct version of transitivity *) +Inductive trans (X : RRel) (x : kcfg) (P : kcfg -> Prop) : Prop := + | tleaf : X x P -> trans X x P + | tdone : P x -> trans X x P + | tstep : forall y, kstep x y -> trans X y P -> trans X x P + | ttrans : forall Q, trans X x Q -> (forall y, Q y -> trans X y P) -> trans X x P + . + +Lemma trans_derived (X : RRel) (trans_stable : F_stable trans X) : stable (trans X). +unfold stable. +induction 1;eauto using stepF. +destruct IHtrans; eauto using StepF,ttrans. +Qed. + +Definition trans_sound (X : RRel) (trans_stable : F_stable trans X) : sound X := + fun x y Hxy => stable_sound (trans_derived trans_stable) _ _ (tleaf _ _ _ Hxy). + +(* some tactics for execution +*) \ No newline at end of file diff --git a/coq/playground/himp/domains.v b/coq/playground/himp/domains.v index 81645d8..79dd6ae 100644 --- a/coq/playground/himp/domains.v +++ b/coq/playground/himp/domains.v @@ -7,6 +7,9 @@ Require Import Setoid. Set Implicit Arguments. +(* Define maps and the syntax used in the definition, + also an equivalence relation on maps and tactics for applying it *) + Inductive Map (Key Elt : Type) : Type := | mapEmpty | mapItem (k : Key) (v : Elt) diff --git a/coq/playground/himp/equate_map_reflection.v b/coq/playground/himp/equate_map_reflection.v new file mode 100644 index 0000000..2237845 --- /dev/null +++ b/coq/playground/himp/equate_map_reflection.v @@ -0,0 +1,308 @@ +Require Import domains. +Require Import String. +Require Import List. +Require Import NPeano. + +Inductive item_rep : Set := + | item (k v : nat) + | submap (m : nat) + . +Inductive map_rep : Set := + | empty + | join (l r : map_rep) + | atom (a : item_rep) + . + +Definition interp_item {K V} keys values submaps (i : item_rep) : Map K V := + match i with + | item k v => + match nth_error keys k, nth_error values v with + | Some k, Some v => k |-> v + | _, _ => mapEmpty + end + | submap m => + match nth_error submaps m with + | Some m => m + | _ => mapEmpty + end + end. + +Definition interp {K V} keys values submaps : map_rep -> Map K V := + fix eval m := match m with + | empty => mapEmpty + | join l r => eval l :* eval r + | atom a => interp_item keys values submaps a + end. + +Definition mapEq {K V} keys values (submaps : list (Map K V)) ml mr : Prop := + interp keys values submaps ml + ~= interp keys values submaps mr. + +Fixpoint merge {A} (lt : A -> A -> bool) (l1 l2 : list A) : list A := + match l1 with + | nil => l2 + | (cons v1 l1') => + (fix scan l2 := + match l2 with + | nil => l1 + | cons v2 l2' => + if lt v1 v2 + then cons v1 (merge lt l1' l2) + else cons v2 (scan l2') + end) l2 + end. + +Definition test1 : merge NPeano.ltb (cons 1 (cons 3 (cons 4 nil))) (cons 0 (cons 2 (cons 5 nil))) + = cons 0 (cons 1 (cons 2 (cons 3 (cons 4 (cons 5 nil))))) + := eq_refl _. + + +Fixpoint removeMatches' {A} (cmp : A -> A -> comparison) (l1 l2 l1_acc l2_acc : list A) : (list A * list A) := + match l1 with + | nil => (rev l1_acc, rev_append l2_acc l2) + | (cons v1 l1') => + (fix scan l2 l2_acc {struct l2} := + match l2 with + | nil => (rev_append l1_acc l1, rev l2_acc) + | cons v2 l2' => + match cmp v1 v2 with + | Lt => removeMatches' cmp l1' l2 (v1::l1_acc) l2_acc + | Eq => removeMatches' cmp l1' l2' l1_acc l2_acc + | Gt => scan l2' (v2::l2_acc) + end + end) l2 l2_acc + end. + +Definition removeMatches {A} cmp (l1 l2 : list A) := removeMatches' cmp l1 l2 nil nil. + +Definition test2 : + removeMatches Nat.compare (cons 1 (cons 3 (cons 4 nil))) (cons 0 (cons 1 (cons 2 (cons 4 nil)))) + = (cons 3 nil, cons 0 (cons 2 nil)) := eq_refl _. + +Definition item_lt (i1 i2 : item_rep) : bool := + match i1, i2 with + | item k v, item k2 v2 => + orb (ltb k k2) (andb (Nat.eqb k k2) (ltb v v2)) + | item _ _, submap _ => true + | submap _, item _ _ => false + | submap m, submap m2 => ltb m m2 + end. +Definition item_cmp (i1 i2 : item_rep) : comparison := + match i1, i2 with + | item k v, item k2 v2 => + match Nat.compare k k2 with + | Eq => Nat.compare v v2 + | o => o + end + | item _ _, submap _ => Lt + | submap _, item _ _ => Gt + | submap m, submap m2 => Nat.compare m m2 + end. + +Lemma item_cmp_prop : forall i1 i2, item_cmp i1 i2 = Eq -> i1 = i2. +Proof. +destruct i1;destruct i2;simpl;unfold Nat.compare; +repeat match goal with [|-context [Compare_dec.nat_compare ?x ?y]] => + destruct (Compare_dec.nat_compare_spec x y) end; +congruence. +Qed. + +Definition joins (l : list map_rep) := fold_right join empty l. +Fixpoint canonicalize (m : map_rep) : list item_rep := + match m with + | empty => nil + | join l r => merge item_lt (canonicalize l) (canonicalize r) + | atom a => cons a nil + end. + +Section Equivalence. + Variables K V : Type. + Variable keys : list K. + Variable values : list V. + Variable submaps : list (Map K V). + + Local Notation int := (interp keys values submaps). + + Lemma merge_join {A} (lt : A -> A -> bool) (f : A -> map_rep) (l1 l2 : list A) : + int (joins (map f (merge lt l1 l2))) + ~= int (join (joins (map f l1)) (joins (map f l2))). + + revert l2; induction l1; intro; simpl. + rewrite equivUnitL; reflexivity. + induction l2; simpl. + rewrite equivUnit; reflexivity. + destruct (lt a a0); simpl. + rewrite IHl1; simpl; equate_maps. + rewrite IHl2; equate_maps. + Qed. + + Lemma canon_equiv : forall m, int m ~= int (joins (map atom (canonicalize m))). + Proof. + induction m;simpl;rewrite ?equivUnit, ?equivUnitL; try reflexivity. + rewrite IHm1, IHm2, merge_join. reflexivity. + Qed. + + Lemma app_equiv l1 l2 : int (joins (l1 ++ l2)) ~= int (joins l1) :* int (joins l2). + induction l1. + simpl; rewrite equivUnitL; reflexivity. + simpl; rewrite IHl1, equivAssoc; reflexivity. + Qed. + + Section RemoveEquiv. + Variable m1 m2 : map_rep. (* Need a rest of map to make this flexible enough *) + + Local Notation build_equiv l1 l2 := (int (joins (m1 :: map atom l1)) ~= int (joins (m2 :: map atom l2))). + + Lemma removeEquivSubmaps (l1 l2 l1_acc l2_acc : list item_rep) : + match removeMatches' item_cmp l1 l2 l1_acc l2_acc with + | (l1', l2') => build_equiv l1' l2' + end -> + build_equiv (rev_append l1_acc l1) (rev_append l2_acc l2). + revert l1_acc l2 l2_acc;induction l1. + simpl; intros; rewrite <- rev_alt; assumption. + induction l2. + simpl; intros; rewrite <- rev_alt; assumption. + intros; simpl in * |- *. + destruct (item_cmp a a0) eqn:Hcmp. + (* Both step? *) + Focus 3. + (* Gt -> use inner IH *) + apply (IHl2 (a0 :: l2_acc)). + apply H. + (* Eq -> goes back to outer IH, with thing dropped *) + specialize (IHl1 _ _ _ H); clear -Hcmp IHl1. + (* rearranging. *) + apply item_cmp_prop in Hcmp. subst a. + rewrite !rev_append_rev, !map_app, !app_equiv in IHl1 |- *. + simpl. + repeat rewrite (equivComAssoc _ (interp_item _ _ _ a0) _). + rewrite IHl1. reflexivity. + (* Lt -> use outer IH? *) + apply IHl1 with (l1_acc := (a :: l1_acc)). + assumption. + Qed. + End RemoveEquiv. + + Lemma reduce_equiv (rep1 rep2 : map_rep) : + match removeMatches item_cmp (canonicalize rep1) (canonicalize rep2) with + | (items1, items2) => + int (joins (map atom items1)) ~= int (joins (map atom items2)) + end + -> int rep1 ~= int rep2. + Proof. + unfold removeMatches; intros. + rewrite (canon_equiv rep1), (canon_equiv rep2). + setoid_rewrite <- equivUnitL. + change (int (joins (empty :: map atom (rev_append nil (canonicalize rep1)))) + ~= int (joins (empty :: map atom (rev_append nil (canonicalize rep2))))). + apply removeEquivSubmaps. + destruct (removeMatches' item_cmp (canonicalize rep1) + (canonicalize rep2) nil nil). + simpl; rewrite H; reflexivity. + Qed. +End Equivalence. + +Definition test3 : forall (k1 k2 : string) (v1 v2 : nat) (m1 : Map string nat), + k1 |-> v1 :* m1 :* k2 |-> v2 ~= m1 :* k2 |-> v2 :* k1 |-> v1. +Proof. +intros. +change + (interp (k1 :: k2 :: nil) (v1 :: v2 ::nil) (m1 :: nil) + (join (atom (item 0 0)) (join (atom (submap 0)) (atom (item 1 1)))) + ~= + interp (k1 :: k2 :: nil) (v1 :: v2 ::nil) (m1 :: nil) + (join (atom (submap 0)) (join (atom (item 1 1)) (atom (item 0 0))))). +apply reduce_equiv. +simpl. +reflexivity. +Qed. + +Ltac inList x xs := + match xs with + | nil => false + | x :: _ => true + | _ :: ?xs' => inList x xs' + end. +Ltac insert x xs := + match inList x xs with + | true => xs + | false => constr:(x :: xs) + end. +Ltac index x xs := + match xs with + | (x :: _) => constr:0 + | (?x' :: ?xs) => let ix := index x xs in constr:(S ix) + end. +Ltac gatherKeys gathered t := + match t with + | ?l :* ?r => let gathered' := gatherKeys gathered l in gatherKeys gathered' r + | (?k |-> _) => insert k gathered + | _ => gathered + end. +Ltac gatherValues gathered t := + match t with + | ?l :* ?r => let gathered' := gatherValues gathered l in gatherValues gathered' r + | (_ |-> ?v) => insert v gathered + | _ => gathered + end. +Ltac gatherSubmaps gathered t := + match t with + | ?l :* ?r => let gathered' := gatherSubmaps gathered l in gatherSubmaps gathered' r + | (_ |-> ?v) => gathered + | ?m => insert m gathered + end. + +Ltac quoteMap ks vs ms t := + match t with + | (@mapEmpty _ _) => empty + | ?l :* ?r => + let repl := quoteMap ks vs ms l in + let repr := quoteMap ks vs ms r in + constr:(join repl repr) + | ?k |-> ?v => + let repk := index k ks in + let repv := index v vs in + constr:(atom (item repk repv)) + | ?m => + let repm := index m ms in + constr:(atom (submap repm)) + end. +Ltac quote_map_equation := match goal with + [|- @MapEquiv ?K ?V ?l ?r ] => + let ks := gatherKeys (@nil K) l in + let ks := gatherKeys ks r in + let vs := gatherValues (@nil V) l in + let vs := gatherValues vs r in + let ms := gatherSubmaps (@nil (Map K V)) l in + let ms := gatherSubmaps ms r in + let repl := quoteMap ks vs ms l in + let repr := quoteMap ks vs ms r in + change (interp ks vs ms repl ~= interp ks vs ms repr) +end. + +Definition test4 : forall (k1 k2 : string) (v1 v2 : nat) (m1 : Map string nat), + k1 |-> v1 :* m1 :* k2 |-> v2 ~= m1 :* k2 |-> v2 :* k1 |-> v1. +Proof. +intros. +quote_map_equation. +apply reduce_equiv. +simpl. +reflexivity. +Qed. + +Ltac map_simpl := quote_map_equation;apply reduce_equiv;simpl. + +Require Import kstyle. +Require Import ZArith. +Coercion EVar : string >-> Exp. +Coercion ECon : Z >-> Exp. + +Ltac name_evars t := + match t with + | ?l ~= ?r => name_evars l; name_evars r + | ?l :* ?r => name_evars l; name_evars r + | ?k |-> ?v => name_evars k; name_evars v + | ?m => try (is_evar m;set m) + end. + + diff --git a/coq/playground/himp/eval_proofs.v b/coq/playground/himp/eval_proofs.v new file mode 100644 index 0000000..cc4d90c --- /dev/null +++ b/coq/playground/himp/eval_proofs.v @@ -0,0 +1,110 @@ +Set Implicit Arguments. + +Require Import String. +Require Import ZArith. + +Require Import domains. +Require Import kstyle. +Require Import coinduction. +Require Import evaluator. + +Coercion EVar : string >-> Exp. +Coercion ECon : Z >-> Exp. + +Function evals n kcfg := + match n with + | 0 => kcfg + | S n => + match eval kcfg with + | Some kcfg' => evals n kcfg' + | None => kcfg + end + end. + +Lemma evals_sound : + forall n c (P : kcfg -> Prop), P (evals n c) -> reaches c P. +Proof. +induction n; simpl; intros; +[|pose proof (eval_sound c); destruct (eval c)]; +eauto using done,step. +Qed. + +Lemma eval_happy' : forall env, + steps (KCfg (kra (SAssign "x" (EPlus "x" "y")) nil) + ("x" |-> 12%Z :* "y" |-> 13%Z :* env) mapEmpty mapEmpty) + (KCfg nil ("x" |-> 25%Z :* "y" |-> 13%Z :* env) mapEmpty mapEmpty). +intros. +repeat (refine (step _ _);[match goal with [|- kstep ?l _] => eapply (eval_sound l) end|]); +instantiate;simpl Zplus;apply done;reflexivity. +Qed. + +Definition gcdProg : Map string Stmt := + "gcd" |-> + SIf (BLe "a" "b") + (SIf (BLe "b" "a") + (Jump "done") + (Seq (SAssign "b" (EMinus "b" "a")) + (Jump "gcd"))) + (Seq (SAssign "a" (EMinus "a" "b")) + (Jump "gcd")). +Lemma label_eval : forall env, + steps (KCfg (kra (Jump "gcd") kdot) + ("a" |-> 12%Z :* "b" |-> 13%Z :* env) mapEmpty gcdProg) + (KCfg (kra (Jump "done") kdot) + ("a" |-> 1%Z :* "b" |-> 1%Z :* env) mapEmpty gcdProg). +intros. apply evals_sound with 307. simpl; repeat split; reflexivity. +Qed. + +(* Some performance tests *) +Definition test_prop := + steps (KCfg (kra (SWhile (BLe 0%Z "x") + (SAssign "x" (EPlus "x" (-1)%Z))) + nil) ("x" |-> 25%Z) mapEmpty mapEmpty) + (KCfg nil ("x" |-> (-1)%Z) mapEmpty mapEmpty). +Ltac kequiv_tac := repeat (apply conj);[reflexivity|simpl;equate_maps ..]. +Ltac finish := apply done;kequiv_tac. + +(* Using tactics alone *) +Lemma loop_test: test_prop. +Proof. +intros; +repeat (refine (step _ _);[econstructor (reflexivity || find_map_entry)|];instantiate;simpl Zplus); +finish. +Qed. + +(* go step by step, but compute successor with eval rather than by tactics *) +Lemma loop_test': test_prop. +Proof. +Ltac step_eval :=refine (step _ _);[match goal with [|- kstep ?l _] => eapply (eval_sound l) end|]. +intros;repeat step_eval;simpl;finish. +Qed. + +(* use multi-step evaluator, reduce with simpl *) +Lemma loop_test_evals_simpl : test_prop. +Proof. +intros;apply (evals_sound 1000);simpl;kequiv_tac. +Qed. + +(* reduce with lazy *) +Lemma loop_test_evals_lazy: test_prop. +Proof. +intros;apply (evals_sound 1000);lazy;kequiv_tac. +Qed. + +(* reduce with cbv *) +Lemma loop_test_evals_cbv: test_prop. +Proof. +intros;apply (evals_sound 1000);cbv;kequiv_tac. +Qed. + +(* reduce with compute *) +Lemma loop_test_evals_compute : test_prop. +Proof. +intros;apply (evals_sound 1000);compute;kequiv_tac. +Qed. + +(* reduce with vm_compute *) +Lemma loop_test_evals_vm_compute : test_prop. +Proof. +intros;apply (evals_sound 1000);vm_compute;kequiv_tac. +Qed. \ No newline at end of file diff --git a/coq/playground/himp/kstep.v b/coq/playground/himp/kstep.v new file mode 100644 index 0000000..349c827 --- /dev/null +++ b/coq/playground/himp/kstep.v @@ -0,0 +1,133 @@ +Require Import ZArith. +Require Import List. +Require Import FMapPositive. +Require Import String. +Open Scope string_scope. + +Require Import domains. + +(* Define the transition relation. + This is split into a separate file because + a bug in Proof General prevents interactively + advancing past definitions as long as the + Inductive block. + *) + +Notation FreezeL f e := (KFreezeE (fun x => f x e)). +Notation FreezeR f e := (KFreezeE (fun x => f e x)). + +Notation "'□' '+' e" := (FreezeL EPlus e) (at level 50) : k_scope. +Notation "e '+' '□'" := (FreezeR EPlus e) (at level 50) : k_scope. +Notation "'□' '-' e" := (FreezeL EMinus e) (at level 50) : k_scope. +Notation "e '-' '□'" := (FreezeR EMinus e) (at level 50) : k_scope. +Notation "'□/' e" := (FreezeL EDiv e) (at level 50): k_scope. +Notation "e '/□'" := (FreezeR EDiv e) (at level 50): k_scope. +Notation "'□<=' e" := (FreezeL BLe e) (at level 70): k_scope. +Notation "i '<=□'" := (FreezeR BLe (ECon i)) (at level 70): k_scope. +Notation "'□==' e" := (FreezeL BEq e) (at level 70): k_scope. +Notation "i '==□'" := (FreezeR BEq (ECon i)) (at level 70): k_scope. +Notation "'□&&' e" := (KFreezeB (fun l => BAnd l e)) (at level 50): k_scope. +Notation "v ':=□'" := (KFreezeE (fun e => SAssign v e)) (at level 70): k_scope. +Notation "'if□then' s1 'else' s2" := (KFreezeB (fun b => SIf b s1 s2)) (at level 20): k_scope. + +Delimit Scope k_scope with K. +Open Scope k_scope. + +Coercion KExp : Exp >-> kitem. +Coercion KBExp : BExp >-> kitem. +Coercion KStmt : Stmt >-> kitem. + +Set Implicit Arguments. + +Notation exp_step step a b := + (forall env henv lenv, + step (KCfg a env henv lenv) + (KCfg b env henv lenv)) (only parsing). + +Notation exp1_step step a b := (forall rest, exp_step step (kra a rest) (kra b rest)) (only parsing). + +Notation heat_step step cool hot ctx := + (forall rest, exp_step step (kra cool rest) (kra hot (kra ctx rest))). +Notation cool_step step hot ctx cool := + (forall rest, exp_step step (kra hot (kra ctx rest)) (kra cool rest)). + +Generalizable Variables rest env erest henv hrest lenv x y i j v r e b s. +Inductive kstep : kcfg -> kcfg -> Prop := + (* evaluation rules *) + | k_amb_left : `(kstep (KCfg (kra (EAmb x y) rest) env henv lenv) + (KCfg (kra x rest) env henv lenv)) + | k_amb_right : `(kstep (KCfg (kra (EAmb x y) rest) env henv lenv) + (KCfg (kra y rest) env henv lenv)) + | k_lookup : `(env ~= (x |-> i :* erest) -> + kstep (KCfg (kra (EVar x) rest) env henv lenv) + (KCfg (kra (ECon i) rest) (x |-> i :* erest) henv lenv)) + | k_load : `(henv ~= (i |-> j :* hrest) -> + kstep (KCfg (kra (ELoad (ECon i)) rest) env henv lenv) + (KCfg (kra (ECon j) rest) env henv lenv)) + | k_assign : `(env ~= (x |-> v :* erest) -> + kstep (KCfg (kra (SAssign x (ECon i)) rest) env henv lenv) + (KCfg rest (x |-> i :* erest) henv lenv)) + | k_hassign : `(henv ~= (i |-> v :* hrest) -> + kstep (KCfg (kra (HAssign (ECon i) (ECon j)) rest) env henv lenv) + (KCfg rest env (i |-> j :* hrest) lenv)) + | k_jump : `(forall l, + lenv ~= (l |-> s :* erest) -> + kstep (KCfg (kra (Jump l) rest) env henv lenv) + (KCfg (kra s kdot) env henv lenv)) + | k_plus : `(exp1_step kstep (EPlus (ECon i) (ECon j)) + (ECon (Zplus i j))) + | k_minus : `(exp1_step kstep (EMinus (ECon i) (ECon j)) + (ECon (Zminus i j))) + | k_div : `(Zneq_bool 0%Z j = true -> + exp1_step kstep (EDiv (ECon i) (ECon j)) + (ECon (Zdiv i j))) + | k_le : `(exp1_step kstep (BLe (ECon i) (ECon j)) + (BCon (Zle_bool i j))) + | k_eq : `(exp1_step kstep (BEq (ECon i) (ECon j)) + (BCon (i =? j)%Z)) + | k_not : `(exp1_step kstep (BNot (BCon b)) (BCon (negb b))) + | k_and_t : `(exp1_step kstep (BAnd (BCon true) b) + b) + | k_and_f : `(exp1_step kstep (BAnd (BCon false) b) + (BCon false)) + | k_skip: `(exp_step kstep (kra Skip rest) + rest) + | k_if_t : `(exp1_step kstep (SIf (BCon true) s1 s2) + s1) + | k_if_f : `(exp1_step kstep (SIf (BCon false) s1 s2) + s2) + | k_while : `(exp1_step kstep (SWhile b s) + (SIf b (Seq s (SWhile b s)) Skip)) + (* heating and cooling *) + | k_cool_e : `(cool_step kstep (ECon i) (KFreezeE e) (e (ECon i))) + | k_cool_b : `(cool_step kstep (BCon b) (KFreezeB e) (e (BCon b))) + (* unary *) + | k_heat_load : `(isEVal e = false -> heat_step kstep (ELoad e) e (KFreezeE ELoad)) + (* plus *) + | k_heat_plus_l : `(isEVal e = false -> heat_step kstep (EPlus e e2) e (□ + e2)) + | k_heat_plus_r : `(isEVal e2 = false -> heat_step kstep (EPlus e e2) e2 (e + □)) + (* minus *) + | k_heat_minus_l : `(isEVal e = false -> heat_step kstep (EMinus e e2) e (□ - e2)) + | k_heat_minus_r : `(isEVal e2 = false -> heat_step kstep (EMinus e e2) e2 (e - □)) + (* div *) + | k_heat_div_l : `(isEVal e = false -> heat_step kstep (EDiv e e2) e (□/ e2)) + | k_heat_div_r : `(isEVal e2 = false -> heat_step kstep (EDiv e e2) e2 (e /□)) + (* le is seqstrict *) + | k_heat_le_l : `(isEVal e = false -> heat_step kstep (BLe e e2) e (□<= e2)) + | k_heat_le_r : `(isEVal e2 = false -> heat_step kstep (BLe (ECon i) e2) e2 (i <=□)) + (* eq is seqstrict *) + | k_heat_eq_l : `(isEVal e = false -> heat_step kstep (BEq e e2) e (□== e2)) + | k_heat_eq_r : `(isEVal e2 = false -> heat_step kstep (BEq (ECon i) e2) e2 (i ==□)) + (* and is only strict in left argument *) + | k_heat_not : `(isBool b = false -> heat_step kstep (BNot b) b (KFreezeB BNot)) + | k_heat_and : `(isBool b1 = false -> heat_step kstep (BAnd b1 b2) b1 (□&& b2)) + (* assign *) + | k_heat_assign : `(isEVal e = false -> heat_step kstep (SAssign x e) e (x :=□)) + (* hassign *) + | k_heat_hassign_l : `(isEVal e = false -> heat_step kstep (HAssign e e2) e (FreezeL HAssign e2)) + | k_heat_hassign_r : `(isEVal e2 = false -> heat_step kstep (HAssign e e2) e2 (FreezeR HAssign e)) + (* if *) + | k_heat_if : `(isBool b = false -> heat_step kstep (SIf b s1 s2) b (if□then s1 else s2)) + (* seq *) + | k_heat_seq : `(heat_step kstep (Seq s1 s2) s1 s2) + . diff --git a/coq/playground/himp/kstyle.v b/coq/playground/himp/kstyle.v index 11bb130..1d05bb0 100644 --- a/coq/playground/himp/kstyle.v +++ b/coq/playground/himp/kstyle.v @@ -1,143 +1,14 @@ -Add LoadPath "../../ml_proof". - Require Import ZArith. Require Import List. -Require Import FMapPositive. Require Import String. -Open Scope string_scope. Require Import domains. +Require Export kstep. -(* -Notation "'□' '+' e" := (Fplusl e) (at level 50) : k_scope. -Notation "e '+' '□'" := (Fplusr e) (at level 50) : k_scope. - *) - -Notation FreezeL f e := (KFreezeE (fun x => f x e)). -Notation FreezeR f e := (KFreezeE (fun x => f e x)). - -Notation "'□' '+' e" := (FreezeL EPlus e) (at level 50) : k_scope. -Notation "e '+' '□'" := (FreezeR EPlus e) (at level 50) : k_scope. -Notation "'□' '-' e" := (FreezeL EMinus e) (at level 50) : k_scope. -Notation "e '-' '□'" := (FreezeR EMinus e) (at level 50) : k_scope. -Notation "'□/' e" := (FreezeL EDiv e) (at level 50): k_scope. -Notation "e '/□'" := (FreezeR EDiv e) (at level 50): k_scope. -Notation "'□<=' e" := (FreezeL BLe e) (at level 70): k_scope. -Notation "i '<=□'" := (FreezeR BLe (ECon i)) (at level 70): k_scope. -Notation "'□==' e" := (FreezeL BEq e) (at level 70): k_scope. -Notation "i '==□'" := (FreezeR BEq (ECon i)) (at level 70): k_scope. -Notation "'□&&' e" := (KFreezeB (fun l => BAnd l e)) (at level 50): k_scope. -Notation "v ':=□'" := (KFreezeE (fun e => SAssign v e)) (at level 70): k_scope. -Notation "'if□then' s1 'else' s2" := (KFreezeB (fun b => SIf b s1 s2)) (at level 20): k_scope. - -Delimit Scope k_scope with K. Open Scope k_scope. -Coercion KExp : Exp >-> kitem. -Coercion KBExp : BExp >-> kitem. -Coercion KStmt : Stmt >-> kitem. - Set Implicit Arguments. -Notation exp_step step a b := - (forall env henv lenv, step (KCfg a env henv lenv) (KCfg b env henv lenv)) (only parsing). - -Notation exp1_step step a b := (forall rest, exp_step step (kra a rest) (kra b rest)) (only parsing). - -Notation heat_step step cool hot ctx := - (forall rest, exp_step step (kra cool rest) (kra hot (kra ctx rest))). -Notation cool_step step hot ctx cool := - (forall rest, exp_step step (kra hot (kra ctx rest)) (kra cool rest)). - -Generalizable Variables rest env erest henv hrest lenv x y i j v r e b s. -Inductive kstep : kcfg -> kcfg -> Prop := - (* evaluation rules *) - | k_amb_left : `(kstep (KCfg (kra (EAmb x y) rest) env henv lenv) - (KCfg (kra x rest) env henv lenv)) - | k_amb_right : `(kstep (KCfg (kra (EAmb x y) rest) env henv lenv) - (KCfg (kra y rest) env henv lenv)) - | k_lookup : `(env ~= (x |-> i :* erest) -> - kstep (KCfg (kra (EVar x) rest) env henv lenv) - (KCfg (kra (ECon i) rest) (x |-> i :* erest) henv lenv)) - | k_load : `(henv ~= (i |-> j :* hrest) -> - kstep (KCfg (kra (ELoad (ECon i)) rest) env henv lenv) - (KCfg (kra (ECon j) rest) env henv lenv)) - | k_assign : `(env ~= (x |-> v :* erest) -> - kstep (KCfg (kra (SAssign x (ECon i)) rest) env henv lenv) - (KCfg rest (x |-> i :* erest) henv lenv)) - | k_hassign : `(henv ~= (i |-> v :* hrest) -> - kstep (KCfg (kra (HAssign (ECon i) (ECon j)) rest) env henv lenv) - (KCfg rest env (i |-> j :* hrest) lenv)) - | k_jump : `(forall l, - lenv ~= (l |-> s :* erest) -> - kstep (KCfg (kra (Jump l) rest) env henv lenv) - (KCfg (kra s kdot) env henv lenv)) - | k_plus : `(exp1_step kstep (EPlus (ECon i) (ECon j)) - (ECon (Zplus i j))) - | k_minus : `(exp1_step kstep (EMinus (ECon i) (ECon j)) - (ECon (Zminus i j))) - | k_div : `(Zneq_bool 0%Z j = true -> - exp1_step kstep (EDiv (ECon i) (ECon j)) - (ECon (Zdiv i j))) - | k_le : `(exp1_step kstep (BLe (ECon i) (ECon j)) - (BCon (Zle_bool i j))) - | k_eq : `(exp1_step kstep (BEq (ECon i) (ECon j)) - (BCon (i =? j)%Z)) - | k_not : `(exp1_step kstep (BNot (BCon b)) (BCon (negb b))) - | k_and_t : `(exp1_step kstep (BAnd (BCon true) b) - b) - | k_and_f : `(exp1_step kstep (BAnd (BCon false) b) - (BCon false)) - | k_skip: `(exp_step kstep (kra Skip rest) - rest) - | k_if_t : `(exp1_step kstep (SIf (BCon true) s1 s2) - s1) - | k_if_f : `(exp1_step kstep (SIf (BCon false) s1 s2) - s2) - | k_while : `(exp1_step kstep (SWhile b s) - (SIf b (Seq s (SWhile b s)) Skip)) - (* heating and cooling *) - | k_cool_e : `(cool_step kstep (ECon i) (KFreezeE e) (e (ECon i))) - | k_cool_b : `(cool_step kstep (BCon b) (KFreezeB e) (e (BCon b))) - (* unary *) - | k_heat_load : `(isEVal e = false -> heat_step kstep (ELoad e) e (KFreezeE ELoad)) - (* plus *) - | k_heat_plus_l : `(isEVal e = false -> heat_step kstep (EPlus e e2) e (□ + e2)) - | k_heat_plus_r : `(isEVal e2 = false -> heat_step kstep (EPlus e e2) e2 (e + □)) - (* minus *) - | k_heat_minus_l : `(isEVal e = false -> heat_step kstep (EMinus e e2) e (□ - e2)) - | k_heat_minus_r : `(isEVal e2 = false -> heat_step kstep (EMinus e e2) e2 (e - □)) - (* div *) - | k_heat_div_l : `(isEVal e = false -> heat_step kstep (EDiv e e2) e (□/ e2)) - | k_heat_div_r : `(isEVal e2 = false -> heat_step kstep (EDiv e e2) e2 (e /□)) - (* le is seqstrict *) - | k_heat_le_l : `(isEVal e = false -> heat_step kstep (BLe e e2) e (□<= e2)) - | k_heat_le_r : `(isEVal e2 = false -> heat_step kstep (BLe (ECon i) e2) e2 (i <=□)) - (* eq is seqstrict *) - | k_heat_eq_l : `(isEVal e = false -> heat_step kstep (BEq e e2) e (□== e2)) - | k_heat_eq_r : `(isEVal e2 = false -> heat_step kstep (BEq (ECon i) e2) e2 (i ==□)) - (* and is only strict in left argument *) - | k_heat_not : `(isBool b = false -> heat_step kstep (BNot b) b (KFreezeB BNot)) - | k_heat_and : `(isBool b1 = false -> heat_step kstep (BAnd b1 b2) b1 (□&& b2)) - (* assign *) - | k_heat_assign : `(isEVal e = false -> heat_step kstep (SAssign x e) e (x :=□)) - (* hassign *) - | k_heat_hassign_l : `(isEVal e = false -> heat_step kstep (HAssign e e2) e (FreezeL HAssign e2)) - | k_heat_hassign_r : `(isEVal e2 = false -> heat_step kstep (HAssign e e2) e2 (FreezeR HAssign e)) - (* if *) - | k_heat_if : `(isBool b = false -> heat_step kstep (SIf b s1 s2) b (if□then s1 else s2)) - (* seq *) - | k_heat_seq : `(heat_step kstep (Seq s1 s2) s1 s2) - . - -Fixpoint notFree' {K} (used : list K) {V} (m : Map K V) (cont : list K -> Prop) {struct m} : Prop := - match m with - | mapEmpty => cont used - | k' |-> _ => ~ In k' used /\ cont (k' :: used) - | l :* r => notFree' used l (fun used' => notFree' used' r cont) - end. -Definition defined {K V} (m : Map K V) : Prop := notFree' nil m (fun _ => True). - Definition kequiv (k1 k2 : kcfg) : Prop := match k1, k2 with | KCfg k1 store1 heap1 labels1, @@ -168,218 +39,23 @@ Add Parametric Relation : kcfg kequiv transitivity proved by kequiv_trans as kequiv_rel. -Lemma kstep_equiv : forall s1 s2, kstep s1 s2 -> - forall s1', kequiv s1 s1' -> exists s2', kstep s1' s2' /\ kequiv s2 s2'. -Proof. -destruct 1;destruct s1';simpl; -intro Hequiv1;destruct Hequiv1 as (Hkcell & Hstore & Henv & Hlabels); -rewrite <- ?Hkcell, ?Hstore, ?Henv, ?Hlabels in * |- *; -refine (ex_intro _ (KCfg _ _ _ _) _); -try solve[(split; -[econstructor (eassumption || reflexivity)|]); -repeat split;(assumption || reflexivity)]. -(* the amb case is trickier *) -eauto using kstep. -Qed. - -CoInductive steps : kcfg -> kcfg -> Prop := - | done : forall c1 c2, kequiv c1 c2 -> steps c1 c2 - | more : forall c1 c1' c2 c3, kequiv c1 c1' -> kstep c1' c2 -> steps c2 c3 -> steps c1 c3 - . - -Lemma steps_equiv : forall s1 s2 s1' s2', - kequiv s1 s1' -> kequiv s2 s2' -> steps s1 s2 -> steps s1' s2'. -Proof. -cofix; intros; destruct H1. -* apply done. rewrite H, H0 in H1. assumption. -* eapply more; eauto. rewrite <- H. assumption. - apply steps_equiv with c2 c3. reflexivity. assumption. assumption. -Qed. - -Lemma steps_append : forall s1 s2 s3, steps s1 s2 -> steps s2 s3 -> steps s1 s3. -Proof. -cofix. -intros. destruct H. -* eapply steps_equiv;[symmetry;eassumption|reflexivity|eassumption]. -* eapply more; eauto. -Qed. - -(* A type that makes transitivity guarded *) -Inductive itsteps (ctsteps : kcfg -> kcfg -> Prop) (c1 c2 : kcfg) : Prop := -| itstep : forall cmid, kstep c1 cmid -> ctsteps cmid c2-> itsteps ctsteps c1 c2 -| ittrans : forall cmid, itsteps ctsteps c1 cmid -> ctsteps cmid c2 -> itsteps ctsteps c1 c2 -. -CoInductive tsteps (c1 c2 : kcfg) : Prop := - | Done : c1 = c2 -> tsteps c1 c2 - | Delay : itsteps tsteps c1 c2 -> tsteps c1 c2. -Inductive PStar {A} (R : A -> A -> Prop) : A -> A -> Prop := - | snil : forall x, PStar R x x - | scons : forall x y z, R x y -> PStar R y z -> PStar R x z - . -Fixpoint ps_append {A : Type} {R : A -> A -> Prop} {c1 c2 c3 : A} (l : PStar R c1 c2) - : PStar R c2 c3 -> PStar R c1 c3 := - match l with - | snil _ => fun r => r - | scons _ _ _ s rest => fun r => scons _ s (ps_append rest r) - end. -Inductive it_nf (c1 c2 : kcfg): Prop := - | it_nf_step : forall {cmid}, kstep c1 cmid -> PStar tsteps cmid c2 -> it_nf c1 c2 - . -Fixpoint it_whnf {c1 c2} (i : itsteps tsteps c1 c2) : it_nf c1 c2 := - match i with - | itstep _ s r => it_nf_step s (scons _ r (snil _ _)) - | ittrans _ l r => - match it_whnf l with - | it_nf_step _ s l' => it_nf_step s (ps_append l' (scons _ r (snil _ _))) - end - end. -Inductive star_ts_nf (c1 c2 : kcfg) : Prop := - | st_nf_done : c1 = c2 -> star_ts_nf c1 c2 - | st_nf_step : forall {cmid}, kstep c1 cmid -> PStar tsteps cmid c2 -> star_ts_nf c1 c2 - . -Fixpoint star_nf {c1 c2} (l : PStar tsteps c1 c2) : star_ts_nf c1 c2 := - match l with - | snil _ => st_nf_done (eq_refl _) - | scons x y z c l' => - match c with - | Done eqxy => - match eq_sym eqxy in _ = x return star_ts_nf x z with - | eq_refl => star_nf l' - end - | Delay i => - match it_whnf i with - | it_nf_step _ s l1 => st_nf_step s (ps_append l1 l') - end - end - end. -CoFixpoint steps_sound {c1 c2} (l : PStar tsteps c1 c2) : steps c1 c2 := - match star_nf l with - | st_nf_done eql => - eq_ind _ (steps c1) (done _ _ (kequiv_refl _)) _ eql - | st_nf_step _ s l' => more _ (kequiv_refl _) s - (steps_sound l') - end. -Definition tsteps_sound {c1 c2} (l : tsteps c1 c2) : steps c1 c2 := - steps_sound (scons _ l (snil _ _ )). - -Ltac finish := - apply done;repeat (apply conj);[reflexivity|simpl;equate_maps ..]. - -Ltac step_rule := refine (more _ (@kequiv_refl _) _ _);[econstructor (reflexivity || (simpl;find_map_entry))|]. -Ltac split_bool bexp := - match bexp with - | negb ?bexp' => split_bool bexp' - | (?x <=? ?y)%Z => destruct (Z.leb_spec x y) - | (?x =? ?y)%Z => destruct (Z.eqb_spec x y) - end. -Ltac split_if := - cbv beta; match goal with - | [|- steps (KCfg (kra (KStmt (SIf (BCon ?test) _ _)) _) _ _ _) _] => split_bool test - | [|- steps (KCfg (kra (KBExp (BAnd (BCon ?test) _)) _) _ _ _) _] => split_bool test - end. - -(* Either solve immediately by using the circularity, - or bail out for manual intervention if the - circularity matches structurally *) -Ltac use_circ circ := - solve[eapply circ; - try (match goal with [|- _ ~= _] => equate_maps;reflexivity end); - instantiate; omega] - || (eapply circ;fail 1). - -Ltac run := repeat (step_rule || split_if || finish). -Ltac run_circ circ := repeat (use_circ circ || (step_rule || split_if || finish)). - -CoFixpoint mult : - forall (x y z k t : Z) erest env heap labels, - (0 <= x)%Z -> - (0 <= y)%Z -> - z = (x * y + k)%Z -> - env ~= ("i" |-> x :* "j" |-> y :* "k" |-> k :* "t" |-> t :* erest) -> - tsteps - (KCfg (kra (SWhile (BLe (ECon 1%Z) (EVar "i")) - (Seq (SAssign "t" (EVar "j")) - (Seq (SAssign "i" (EPlus (EVar "i") (ECon (-1)%Z))) - (SWhile (BLe (ECon 1%Z) (EVar "t")) - (Seq (SAssign "k" (EPlus (EVar "k") (ECon 1%Z))) - (SAssign "t" (EPlus (EVar "t") (ECon (-1)%Z)))))))) - (kra (SAssign "t" (ECon 0%Z)) - kdot)) - env heap labels) - (KCfg kdot - ("i" |-> 0%Z :* "j" |-> y%Z :* "k" |-> z :* "t" |-> 0%Z :* erest) heap labels) -with mult_sum : - forall (x y z : Z) krest erest env heap labels, - (0 <= y)%Z -> - z = (x + y)%Z -> - env ~= ("k" |-> x :* "t" |-> y :* erest) -> - tsteps - (KCfg (kra - (SWhile (BLe (ECon 1%Z) (EVar "t")) - (Seq (SAssign "k" (EPlus (EVar "k") (ECon 1%Z))) - (SAssign "t" (EPlus (EVar "t") (ECon (-1)%Z))))) - krest) - env heap labels) - (KCfg krest - ("k" |-> z :* "t" |-> 0%Z :* erest) heap labels). -Ltac tstep := refine (Delay (itstep _ _ _ _));[econstructor (solve[reflexivity || find_map_entry])|]. -Ltac tsplit_if := cbv beta; (* reduce redexes left from plugging *) - match goal with - | [|- tsteps (KCfg (kra (KStmt (SIf (BCon (?x <=? ?y)%Z) _ _)) _) _ _ _) _] => - pose proof (Zle_cases x y); destruct (x <=? y)%Z - end. -Proof. -(* Outer *) -* intros;repeat tstep. tsplit_if. -(* harder true case *) -+ -simpl in H1; subst z. -do 14 tstep. -eapply Delay. eapply ittrans. - - eapply itstep;[solve[econstructor(reflexivity||equate_maps)]|]. - eapply mult_sum; clear mult mult_sum. - Focus 3. - instantiate (3:=k). - instantiate (2:=y). - instantiate (1:="j" |-> y :* "i" |-> (x + -1)%Z :* erest). - equate_maps. - assumption. - simpl. reflexivity. - - eapply mult; clear mult mult_sum. - Focus 4. - instantiate (3:=(x + -1)%Z). - instantiate (2:=(k + y)%Z). - instantiate (1:=0%Z). - equate_maps. - omega. - omega. - ring. - -(* easy false case *) -+ clear mult mult_sum. - repeat tstep. - apply Done. - replace x with 0%Z in * |- * by omega. - match goal with [|- ?l = ?r] => assert (kequiv l r) end. - solve[repeat split;try solve[equate_maps]]. - admit. - -(* Inner *) -* clear mult. - intros. - repeat tstep. tsplit_if. - - - do 17 tstep. - eapply mult_sum; clear mult_sum; try solve[equate_maps]; omega. - - clear mult_sum. - repeat tstep. - apply Done. - replace y with 0%Z by omega. - replace x with z by omega. - (* now they are equivalent, but ksteps was currently - defined in terms of eq rather than kequiv. - So, assert kequiv to prove we can, and then admit the eq *) - match goal with [|- ?l = ?r] => assert (kequiv l r) end. - + solve[repeat split;try solve[equate_maps]]. - + admit. +Create HintDb kstep_equiv_hints discriminated. +Ltac use_map_hyp := + match goal with + [Heq: ?l ~= ?l', Hstruct: ?l ~= ?r |- ?l' ~= ?r'] => unify r r'; + eexact (equivTrans (equivSym Heq) Hstruct) + end. +Hint Constructors kstep : kstep_equiv_hints. +Hint Extern 0 (kequiv _ _) => + split;[reflexivity|(split;[|split]); + (assumption || apply equivRefl || use_map_hyp)] + : kstep_equiv_hints. +Hint Resolve equivRefl : kstep_equiv_hints. +Hint Extern 3 (_ ~= _) => use_map_hyp : kstep_equiv_hints. + +Lemma kstep_equiv : forall c1 c1' c2, + kequiv c1 c1' -> kstep c1 c2 -> exists c2', kstep c1' c2' /\ kequiv c2 c2'. +intros. +destruct c1';destruct H0;unfold kequiv in H;destruct H as [<- [? [? ?]]]; +try solve[eauto with kstep_equiv_hints]. Qed. \ No newline at end of file diff --git a/coq/playground/himp/mult_proof.v b/coq/playground/himp/mult_proof.v new file mode 100644 index 0000000..d5e70fa --- /dev/null +++ b/coq/playground/himp/mult_proof.v @@ -0,0 +1,97 @@ +Require Import ZArith. +Require Import List. +Require Import FMapPositive. +Require Import String. +Open Scope string_scope. + +Require Import domains. +Require Import kstyle. +Require Import steps. + +Set Implicit Arguments. + +(* Test the transitivity stuff. + We'll want to automate this *) +CoFixpoint mult : + forall (x y z k t : Z) erest env heap labels, + (0 <= x)%Z -> + (0 <= y)%Z -> + z = (x * y + k)%Z -> + env ~= ("i" |-> x :* "j" |-> y :* "k" |-> k :* "t" |-> t :* erest) -> + tsteps + (KCfg (kra (SWhile (BLe (ECon 1%Z) (EVar "i")) + (Seq (SAssign "t" (EVar "j")) + (Seq (SAssign "i" (EPlus (EVar "i") (ECon (-1)%Z))) + (SWhile (BLe (ECon 1%Z) (EVar "t")) + (Seq (SAssign "k" (EPlus (EVar "k") (ECon 1%Z))) + (SAssign "t" (EPlus (EVar "t") (ECon (-1)%Z)))))))) + (kra (SAssign "t" (ECon 0%Z)) + kdot)) + env heap labels) + (KCfg kdot + ("i" |-> 0%Z :* "j" |-> y%Z :* "k" |-> z :* "t" |-> 0%Z :* erest) heap labels) +with mult_sum : + forall (x y z : Z) krest erest env heap labels, + (0 <= y)%Z -> + z = (x + y)%Z -> + env ~= ("k" |-> x :* "t" |-> y :* erest) -> + tsteps + (KCfg (kra + (SWhile (BLe (ECon 1%Z) (EVar "t")) + (Seq (SAssign "k" (EPlus (EVar "k") (ECon 1%Z))) + (SAssign "t" (EPlus (EVar "t") (ECon (-1)%Z))))) + krest) + env heap labels) + (KCfg krest + ("k" |-> z :* "t" |-> 0%Z :* erest) heap labels). +Proof. +(* Outer *) +* intros;repeat tstep. tsplit_if. +(* harder true case *) ++ +simpl in H1; subst z. +do 14 tstep. +eapply Delay. eapply ittrans. + - eapply itstep;[solve[econstructor(reflexivity||equate_maps)]|]. + eapply mult_sum; clear mult mult_sum. + Focus 3. + instantiate (3:=k). + instantiate (2:=y). + instantiate (1:="j" |-> y :* "i" |-> (x + -1)%Z :* erest). + equate_maps. + assumption. + simpl. reflexivity. + - eapply mult; clear mult mult_sum. + Focus 4. + instantiate (3:=(x + -1)%Z). + instantiate (2:=(k + y)%Z). + instantiate (1:=0%Z). + equate_maps. + omega. + omega. + ring. + +(* easy false case *) ++ clear mult mult_sum. + repeat tstep. + apply Done. + replace x with 0%Z in * |- * by omega. + solve[repeat split;try solve[equate_maps]]. + +(* Inner *) +* clear mult. + intros. + repeat tstep. tsplit_if. + - + do 17 tstep. + eapply mult_sum; clear mult_sum; try solve[equate_maps]; omega. + - clear mult_sum. + repeat tstep. + apply Done. + replace y with 0%Z by omega. + replace x with z by omega. + (* now they are equivalent, but ksteps was currently + defined in terms of eq rather than kequiv. + So, assert kequiv to prove we can, and then admit the eq *) + solve[repeat split;try solve[equate_maps]]. +Qed. \ No newline at end of file diff --git a/coq/playground/himp/simple_proofs.v b/coq/playground/himp/simple_proofs.v index cddf5dd..5139eb9 100644 --- a/coq/playground/himp/simple_proofs.v +++ b/coq/playground/himp/simple_proofs.v @@ -6,50 +6,160 @@ Open Scope string_scope. Require Import domains. Require Import kstyle. -Require Import evaluator. +Require Import coinduction. Coercion EVar : string >-> Exp. Coercion ECon : Z >-> Exp. Open Scope Z_scope. + +(* One thing to try is defining a simple wrapper to turn a parameterized rule + into a relation, see if we can get it automatically *) + +Ltac kequiv_tac := repeat (apply conj);[reflexivity|simpl;equate_maps ..]. +Ltac kstep_tac := econstructor(reflexivity || (simpl;find_map_entry)). + +(* +(* Either solve immediately by using the circularity, + or bail out for manual intervention if the + circularity matches structurally *) +Ltac use_circ circ := + solve[eapply circ; + try (match goal with [|- _ ~= _] => equate_maps;reflexivity end); + instantiate; omega] + || (eapply circ;fail 1). + +Ltac run := repeat (step_rule || split_if || finish). +Ltac run_circ circ := repeat (use_circ circ || (step_rule || split_if || finish)). + +Ltac tstep := refine (Delay (itstep _ _ _ _));[econstructor (solve[reflexivity || find_map_entry])|]. +Ltac tsplit_if := cbv beta; (* reduce redexes left from plugging *) + match goal with + | [|- tsteps (KCfg (kra (KStmt (SIf (BCon (?x <=? ?y)%Z) _ _)) _) _ _ _) _] => + pose proof (Zle_cases x y); destruct (x <=? y)%Z + end. + *) + +Notation basic_goal rel := + (forall env, + rel (KCfg (kra (SAssign "x" (EPlus "x" "y")) nil) + (env :* "x" |-> 12%Z :* "y" |-> 13%Z) mapEmpty mapEmpty) + (kequiv (KCfg nil (env :* "x" |-> 25%Z :* "y" |-> 13%Z) mapEmpty mapEmpty))). +(* Very basic example, no heaps or labels, and even using derived rules *) +Lemma direct_coinduction : basic_goal reaches. +intros. +repeat (eapply step;[econstructor (reflexivity || find_map_entry)|]);apply done. +repeat split;equate_maps. +Qed. + +(* Using tactics for kstep, kequiv *) +Lemma basic_tacs : basic_goal reaches. +intros. +repeat (eapply step;[kstep_tac|]);apply done;kequiv_tac. +Qed. + +Ltac steps_run := repeat (eapply step;[kstep_tac|]);apply done;kequiv_tac. + +(* Now using derived rules *) + +(* Try to either finish immediately or take a step at a stepF goal *) +Ltac first_step := (apply DoneF;kequiv_tac) || (eapply StepF;[kstep_tac|]). +Ltac by_rules rules := let H := + fresh in assert (sound rules) as H;[apply trans_sound;destruct 1;first_step|intros;apply H;constructor]. + +Inductive basic_rule : RRel := BasicGoal : basic_goal basic_rule. + +Lemma derived_rules : basic_goal reaches. +by_rules basic_rule. +repeat (eapply tstep;[kstep_tac|]);apply tdone;kequiv_tac. +Qed. + +(* Make a basic run tactic *) +Ltac tstep_tac := eapply tstep;[kstep_tac|]. +Ltac tfinish_tac := solve[apply tdone;kequiv_tac]. + +Ltac trun_basic := repeat tstep_tac;try tfinish_tac. + +Lemma trun_basic_test : basic_goal reaches. +by_rules basic_rule;trun_basic. +Qed. + +Notation heap_goal rel := + (forall p env, rel (KCfg (kra (HAssign "x" (EPlus (ELoad "x") 1%Z)) nil) + (env :* "x" |-> p) (p |-> 12%Z) mapEmpty) + (kequiv (KCfg nil (env :* "x" |-> p) (p |-> 13%Z) mapEmpty))). + +Inductive heap_rule : RRel := HeapGoal : heap_goal heap_rule. +(* Now an example program that has a heap *) +Lemma heap_test : heap_goal reaches. +Proof. +by_rules heap_rule;trun_basic. +Qed. + +(* Slightly more compilicated example, needing to split. *) Definition step (state event : Z) := - match event, state with + match state, event with | Z0, Z0 => 1 | _, _ => 0 end. +Lemma step_ZZ : forall s e, s = 0 -> e = 0 -> step s e = 1. +intros;subst;reflexivity. Qed. +Lemma step_N1 : forall s e, s <> 0 -> step s e = 0. +intros;destruct s;simpl;congruence. Qed. +Lemma step_N2 : forall s e, e <> 0 -> step s e = 0. +intros;destruct s;destruct e;simpl;congruence. Qed. +Create HintDb step_simpl discriminated. +Hint Rewrite step_ZZ step_N1 step_N2 using assumption: step_simpl. -Lemma update_function : forall state addr event, - steps (KCfg (kra (SIf +Notation split_goal rel := (forall state addr event, + rel (KCfg (kra (SIf (BAnd (BEq (ELoad "state") 0) (BEq "event" 0)) (HAssign "state" 1) (HAssign "state" 0)) nil) ("event" |-> event :* "state" |-> addr) (addr |-> state) mapEmpty) - (KCfg nil - ("event" |-> event :* "state" |-> addr) (addr |-> (step state event)) mapEmpty). + (kequiv (KCfg nil + ("event" |-> event :* "state" |-> addr) (addr |-> (step state event)) mapEmpty))). +Inductive split_rules : RRel := SplitGoal : split_goal split_rules. + +(* First split manually *) +Lemma manual_split : split_goal reaches. Proof. -intros. -run;destruct state;destruct event; -simpl;(congruence || reflexivity). +by_rules split_rules;trun_basic. +(* Gets stuck at split *) +destruct state;trun_basic. +destruct event;trun_basic. Qed. Close Scope Z_scope. -Lemma heap_test : forall p env, - steps (KCfg (kra (HAssign "x" (EPlus (ELoad "x") 1%Z)) nil) - (env :* "x" |-> p) (p |-> 12%Z) mapEmpty) - (KCfg nil (env :* "x" |-> p) (p |-> 13%Z) mapEmpty). +Ltac split_bool bexp := + match bexp with + | negb ?bexp' => split_bool bexp' + | (?x <=? ?y)%Z => destruct (Z.leb_spec x y) + | (?x =? ?y)%Z => destruct (Z.eqb_spec x y) + end. +Ltac tsplit_if := + cbv beta; match goal with + | [|- trans _ (KCfg (kra (KStmt (SIf (BCon ?test) _ _)) _) _ _ _) _] => split_bool test + | [|- trans _ (KCfg (kra (KBExp (BAnd (BCon ?test) _)) _) _ _ _) _] => split_bool test + end. + +Ltac trun_split finish_simpl := repeat (tstep_tac || tsplit_if);finish_simpl;try tfinish_tac. + +Lemma auto_split : split_goal reaches. Proof. -intros. -repeat (refine (more _ (@kequiv_refl _) _ _);[econstructor(reflexivity||find_map_entry)|]). -finish. -Qed. +by_rules split_rules;trun_split ltac:(autorewrite with step_simpl). +Qed. +Close Scope Z_scope. +(* List reverse *) Definition listrev := (SWhile (BNot (BEq 0%Z "p")) - (Seq (SAssign "next" (ELoad (EPlus "p" 1%Z))) + (Seq (SAssign "next" (ELoad (EPlus "p" 1%Z))) (Seq (HAssign (EPlus "p" 1%Z) "q") (Seq (SAssign "q" "p") (SAssign "p" "next"))))). +(* Representation predicate *) Fixpoint listrep (l : list Z) (p : Z) (m : Map Z Z) : Prop := match l with | nil => p = 0%Z /\ m ~= mapEmpty @@ -60,20 +170,20 @@ Fixpoint listrep (l : list Z) (p : Z) (m : Map Z Z) : Prop := /\ listrep l' next m' end. +(* Ltac same_eprefix H := match goal with [ H : exists _ : ?A , _ |- exists _ : ?A , _ ] => let x := fresh "x" in destruct H as [x H]; exists x end. - +*) + Lemma listrep_equiv : forall l p m m', m ~= m' -> listrep l p m -> listrep l p m'. destruct l;simpl; intuition. -rewrite <- H; assumption. -repeat same_eprefix H2. -intuition. -rewrite <- H; assumption. +setoid_rewrite <- H; assumption. Qed. +(* Test a concrete execution of list reverse *) Lemma rev_test : forall lenv, steps (KCfg (kra listrev nil) ("p" |-> 1 :* "q" |-> 0 :* "next" |-> 1)%Z @@ -88,18 +198,9 @@ Lemma rev_test : forall lenv, 5 |-> 14 :* 6 |-> 3)%Z lenv). Proof. -intros;repeat step_rule;finish. +intros;steps_run. Qed. -(* For a generic statement about reverse, we would like - to have an existential about the address the reversed - list starts at, need a different sort of reaching - to let us put the existential where we like. *) - -CoInductive reaches (s : kcfg) (phi : kcfg -> Prop) : Prop := - | r_done : phi s -> reaches s phi - | r_more : forall s', kstep s s' -> reaches s' phi -> reaches s phi. - (* Brute force attempt to simplify all representation predicates *) Ltac simplify_listrep := repeat match goal with @@ -112,6 +213,22 @@ Ltac simplify_listrep := repeat try (rewrite H in * |- *;clear H heap) end. +(* Need to adjust tactics to stop at circularities, and maybe do something + about automatically cleaning up lists *) + +(* Idea 1: assume circularities have non-overlapping in left-hand side, + so we can commit to the first that unifies and (fail 1) if we couldn't + satisfy it's hypotheses *) +(* Idea 2: add into the run cycle a tactic that recognizes lookups on an + address registered with a representation predicate, and unfolds/splits to + make progress + *) +(* Idea 3: probably folding can be handled by writing invariant rules with + folded conclusions, and then we only have to deal with it at the finish + while trying to validate that rule + *) + +(* Ltac stop_at_circ circ := (eapply circ; fail 1). (* add to find_map_entry a thing that unfolds/splits *) Ltac r_step := (eapply r_more;[solve[econstructor(reflexivity||find_map_entry)]|]). @@ -163,39 +280,6 @@ simpl. split;[congruence|]. eexists;eexists;split;[|eassumption]. equate_maps. Qed. -Function evals n kcfg := - match n with - | 0 => kcfg - | S n => - match eval kcfg with - | Some kcfg' => evals n kcfg' - | None => kcfg - end - end. - -Lemma evals_sound : - forall n c1 c2, - kequiv (evals n c1) c2 -> steps c1 c2. -Proof. -induction n; simpl; intros c1 c2. -apply done. -pose proof (eval_sound c1). -destruct (eval c1). -intro. -apply more with c1 k. reflexivity. -assumption. apply IHn. assumption. -apply done. -Qed. - -Lemma eval_happy : forall env, - steps (KCfg (kra (SAssign "x" (EPlus "x" "y")) nil) - (env :* "x" |-> 12%Z :* "y" |-> 13%Z) mapEmpty mapEmpty) - (KCfg nil (env :* "x" |-> 25%Z :* "y" |-> 13%Z) mapEmpty mapEmpty). -intros. -repeat (refine (more _ (@kequiv_refl _) _ _);[econstructor (reflexivity || find_map_entry)|]); -simpl Zplus; finish. -Qed. - (* Try "quote" on the env *) (* Use a mixed coinductive sequencing to use loop invariants? *) @@ -215,60 +299,4 @@ CoFixpoint sum : ("i" |-> 0%Z :* "j" |-> z%Z :* erest) heap labels). intros; step_rule;run_circ sum. Qed. - -Lemma eval_happy' : forall env, - steps (KCfg (kra (SAssign "x" (EPlus "x" "y")) nil) - ("x" |-> 12%Z :* "y" |-> 13%Z :* env) mapEmpty mapEmpty) - (KCfg nil ("x" |-> 25%Z :* "y" |-> 13%Z :* env) mapEmpty mapEmpty). -intros; -repeat (refine (more _ (@kequiv_refl _) _ _);[match goal with [|- kstep ?l _] => eapply (eval_sound l) end|]); -simpl Zplus; finish. -Qed. - -Definition gcdProg : Map string Stmt := - "gcd" |-> - SIf (BLe "a" "b") - (SIf (BLe "b" "a") - (Jump "done") - (Seq (SAssign "b" (EMinus "b" "a")) - (Jump "gcd"))) - (Seq (SAssign "a" (EMinus "a" "b")) - (Jump "gcd")). -Lemma label_eval : forall env, - steps (KCfg (kra (Jump "gcd") kdot) - ("a" |-> 12%Z :* "b" |-> 13%Z :* env) mapEmpty gcdProg) - (KCfg (kra (Jump "done") kdot) - ("a" |-> 1%Z :* "b" |-> 1%Z :* env) mapEmpty gcdProg). -intros. apply evals_sound with 307; simpl; repeat split; reflexivity. -Qed. - -(* Some performance tests *) -Lemma loop_test: - steps (KCfg (kra (SWhile (BLe 0%Z "x") - (SAssign "x" (EPlus "x" (-1)%Z))) - nil) ("x" |-> 25%Z) mapEmpty mapEmpty) - (KCfg nil ("x" |-> (-1)%Z) mapEmpty mapEmpty). -Proof. -intros; -repeat (refine (more _ (@kequiv_refl _) _ _);[econstructor (reflexivity || find_map_entry)|];instantiate;simpl Zplus); -finish. -Qed. - -Lemma loop_test': - steps (KCfg (kra (SWhile (BLe 0%Z "x") - (SAssign "x" (EPlus "x" (-1)%Z))) - nil) ("x" |-> 25%Z) mapEmpty mapEmpty) - (KCfg nil ("x" |-> (-1)%Z) mapEmpty mapEmpty). -Proof. -Ltac step_eval :=refine (more _ (@kequiv_refl _) _ _);[match goal with [|- kstep ?l _] => eapply (eval_sound l) end|]. -intros;repeat step_eval;simpl;finish. -Qed. - -Lemma loop_test'': - steps (KCfg (kra (SWhile (BLe (ECon 0) (EVar "x")) - (SAssign "x" (EPlus (EVar "x") (ECon (-1)%Z)))) - nil) ("x" |-> 25%Z) mapEmpty mapEmpty) - (KCfg nil ("x" |-> (-1)%Z) mapEmpty mapEmpty). -Proof. -intros;apply (evals_sound 1000);lazy;repeat (apply conj);[reflexivity|simpl;equate_maps ..]. -Qed. \ No newline at end of file + *) \ No newline at end of file