Use more semantic style of coinduction

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

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.

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
+*)

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)