array

examples/BasicDemos/Demo.ml

@@ -531,9 +531,15 @@ type ('a,'b) algb_erase =
 (********************************************************************)
 (* ** Type record *)
 
-type recorda = { recorda1 : int; recorda2 : int }
+type recorda = { 
+   mutable recorda1 : int; 
+   mutable recorda2 : int }
 
-type ('a,'b) recordb = { recordb1 : 'a ; recordb2 : 'b -> 'b }
+(*----*)
+
+type ('a,'b) recordb = 
+  { mutable recordb1 : 'a ; 
+    mutable recordb2 : 'b -> 'b }
 
 (* not supported: record overloading of fields 
   -- else would need to prefix all fields with the type... *)
@@ -542,10 +548,27 @@ type ('a,'b) recordb = { recordb1 : 'a ; recordb2 : 'b -> 'b }
 (********************************************************************)
 (* ** Type mutual *)
 
+(*----*)
+
 type typereca1 = | Typereca_1 of typereca2
  and typereca2 = | Typereca_2 of typereca1
 
-(* not supported: recursive definition of inductive and record
+(*----*)
+
+(* not supported: recursive definitions using abbreviation
+
+type typerecb1 = | Typerecb_1 of typerecb2
+ and typerecb2 = typerecb1 list
+
+   --> the work around by inlining, e.g.:
+*)
+
+type typerecc1 = | Typerecc_1 of typerecc1 list
+type typerecc2 = typerecc1 list
+
+(*----*)
+
+(* not supported: recursive definition of inductive and pure records
    -- technically could be supported, if the record was encoded
       on the fly into a coq mutual inductive
 type typerecb1 = | Typerecb_1 of typerecb2
@@ -557,16 +580,17 @@ type typerecb1 = | Typerecb_1 of typerecb2
 type 'a typerecb2 = { typerecb_2 : 'a }
 type typerecb1 = | Typerecb_1 of typerecb1 typerecb2
 
-(* not supported: recursive definitions using abbreviation
-
-type typerecb1 = | Typerecb_1 of typerecb2
- and typerecb2 = typerecb1 list
+(*----*)
 
-   --> the work around by inlining, e.g.:
-*)
+(* Circularity between mutable records and inductive is broken 
+   through the indirection at type loc *)
 
-type typerecc1 = | Typerecc_1 of typerecc1 list
-type typerecc2 = typerecc1 list
+type 'a typerecd1 = { typerecd1_f : 'a typerecd2 }
+and 'a typerecd2 = 
+   | Typerecd_2a 
+   | Typerecd_2b of 'a typerecd1 
+   | Typerecd_2c of 'a typerecd3 
+type 'a typerecd3 = { typerecd3_f : 'a typerecd2 }
 
 
 
@@ -618,3 +642,4 @@ end
 
 (********************************************************************)
 (* ** TODO: import of auxiliary files, like in examples/DemoMake *)
+

examples/BasicDemos/Demo_proof.v

@@ -5,120 +5,9 @@ Require Import Demo_ml.
 Require Import Stdlib. 
 
 
-Ltac get_fun_arg E ::=
-  match E with
-  | ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X7 ?X => constr:((X1 X2 X3 X4 X5 X6 X7,X))
-  | ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X => constr:((X1 X2 X3 X4 X5 X6,X))
-  | ?X1 ?X2 ?X3 ?X4 ?X5 ?X => constr:((X1 X2 X3 X4 X5,X))  
-  | ?X1 ?X2 ?X3 ?X4 ?X => constr:((X1 X2 X3 X4,X))
-  | ?X1 ?X2 ?X3 ?X => constr:((X1 X2 X3,X)) 
-  | ?X1 ?X2 ?X => constr:((X1 X2,X))
-  | ?X1 ?X => constr:((X1,X))
-  end.
 
 
 
-(********************************************************************)
-(* ** Records *)
-
-Lemma sitems_build_spec : forall (A:Type) (n:int),
-  app sitems_build [n] \[] (fun r => r ~> `{ nb' := n; items' := @nil A }).
-Proof using. xcf_go~. Qed.
-
-Lemma sitems_get_nb_spec : forall (A:Type) (r:loc) (n:int),
-  app_keep sitems_get_nb [r]  
-     (r ~> `{ nb' := n; items' := @nil A })
-     \[= n].
-Proof using.
-  dup 3. 
-  { intros A. xcf_show as R. applys (R A). xgo~. }
-  { xcf_show as R. unfold sitems_ in R. specializes R unit. xgo~. }
-  { xcf_go~. Unshelve. solve_type. }
-Qed.  (* TODO: can we do better than a manual unshelve for dealing with unused type vars? *)
-
-Lemma sitems_incr_nb_spec : forall (A:Type) (L:list A) (r:loc) (n:int),
-  app sitems_incr_nb [r]  
-     (r ~> `{ nb' := n; items' := L })
-     (# (r ~> `{ nb' := n+1; items' := L })).
-Proof using.
-  dup 2.
-  { xcf. xapps. xapp. Unshelve. solve_type. } 
-  { xcf_go*. Grab Existential Variables. solve_type. }
-Qed.
-
-Lemma sitems_length_item_spec : forall (A:Type) (r:loc) (L:list A) (n:int),
-  app_keep sitems_length_items [r]  
-     (r ~> `{ nb' := n; items' := L })
-     \[= LibListZ.length L ].
-Proof using.
-  dup 2.
-  { xcf. xapps. xrets. }
-  { xcf_go*. }
-Qed.
-
-Definition Sitems A (L:list A) r := 
-  Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ].
-
-Lemma sitems_push_spec : forall (A:Type) (r:loc) (L:list A) (x:A),
-  app sitems_push [x r] (r ~> Sitems L) (# r ~> Sitems (x::L)).
-Proof using.
-  xcf. xunfold Sitems. xextract ;=> n E. 
-  xapps. xapps. xapps. xapp. xsimpl. rew_list; math.
-Qed.
-
-(** Demo of [xfocus] and [xunfocus] *)
-
-Lemma Sitems_focus : forall r A (L:list A),
-  r ~> Sitems L ==> 
-  Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ].
-Proof using. intros. xunfolds~ Sitems. Qed.
-
-Lemma Sitems_unfocus : forall r A (L:list A) (n:int),
-  n = LibListZ.length L ->
-  r ~> `{ nb' := n; items' := L } ==> 
-  r ~> Sitems L.
-Proof using. intros. xunfolds~ Sitems. Qed.
-
-Implicit Arguments Sitems_unfocus [].
-
-Hint Extern 1 (Register focus (Sitems _)) => 
-  Provide Sitems_focus.
-Hint Extern 1 (Register unfocus (record_repr `{ nb' := _; items' := _ }')) =>  
-  Provide Sitems_unfocus.
-
-(** - [xfocusx t]  is short for [xfocus t; xextract] 
-    - [xfocusx t]  is short for [xfocus t; xextracts] *)
-
-Tactic Notation "xfocusx" constr(t) :=
-  xfocus t; xextract.
-
-Tactic Notation "xfocusxs" constr(t) :=
-  xfocus t; xextracts.
-
-Lemma sitems_push_spec' : forall (A:Type) (r:loc) (L:list A) (x:A),
-  app sitems_push [x r] (r ~> Sitems L) (# r ~> Sitems (x::L)).
-Proof using. 
-  xcf. dup 2.
-  { xfocus r. xextract ;=> n E. skip. } 
-  { xfocusx r ;=> n E. xapps. xapps. xapps. xapp.
-    xunfocus r. rew_list; math. xsimpl~. }
-Qed.
-
-
-
-(********************************************************************)
-(* ** Arrays *)
-
-Lemma array_ops () =
-  let t = Array.make 3 0 in
-  let _x = t.(1) in
-  t.(2) <- 4;
-  let _y = t.(2) in
-  let _z = t.(1) in
-  Array.length t
-Proof using.
-  xcf.
-Qed.
 
 
 
@@ -828,6 +717,111 @@ Qed.
 
 
 
+(********************************************************************)
+(* ** Records *)
+
+Lemma sitems_build_spec : forall (A:Type) (n:int),
+  app sitems_build [n] \[] (fun r => r ~> `{ nb' := n; items' := @nil A }).
+Proof using. xcf_go~. Qed.
+
+Lemma sitems_get_nb_spec : forall (A:Type) (r:loc) (n:int),
+  app_keep sitems_get_nb [r]  
+     (r ~> `{ nb' := n; items' := @nil A })
+     \[= n].
+Proof using.
+  dup 3. 
+  { intros A. xcf_show as R. applys (R A). xgo~. }
+  { xcf_show as R. unfold sitems_ in R. specializes R unit. xgo~. }
+  { xcf_go~. Unshelve. solve_type. }
+Qed.  (* TODO: can we do better than a manual unshelve for dealing with unused type vars? *)
+
+Lemma sitems_incr_nb_spec : forall (A:Type) (L:list A) (r:loc) (n:int),
+  app sitems_incr_nb [r]  
+     (r ~> `{ nb' := n; items' := L })
+     (# (r ~> `{ nb' := n+1; items' := L })).
+Proof using.
+  dup 2.
+  { xcf. xapps. xapp. Unshelve. solve_type. } 
+  { xcf_go*. Grab Existential Variables. solve_type. }
+Qed.
+
+Lemma sitems_length_item_spec : forall (A:Type) (r:loc) (L:list A) (n:int),
+  app_keep sitems_length_items [r]  
+     (r ~> `{ nb' := n; items' := L })
+     \[= LibListZ.length L ].
+Proof using.
+  dup 2.
+  { xcf. xapps. xrets. }
+  { xcf_go*. }
+Qed.
+
+Definition Sitems A (L:list A) r := 
+  Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ].
+
+Lemma sitems_push_spec : forall (A:Type) (r:loc) (L:list A) (x:A),
+  app sitems_push [x r] (r ~> Sitems L) (# r ~> Sitems (x::L)).
+Proof using.
+  xcf. xunfold Sitems. xextract ;=> n E. 
+  xapps. xapps. xapps. xapp. xsimpl. rew_list; math.
+Qed.
+
+(** Demo of [xfocus] and [xunfocus] *)
+
+Lemma Sitems_focus : forall r A (L:list A),
+  r ~> Sitems L ==> 
+  Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ].
+Proof using. intros. xunfolds~ Sitems. Qed.
+
+Lemma Sitems_unfocus : forall r A (L:list A) (n:int),
+  n = LibListZ.length L ->
+  r ~> `{ nb' := n; items' := L } ==> 
+  r ~> Sitems L.
+Proof using. intros. xunfolds~ Sitems. Qed.
+
+Implicit Arguments Sitems_unfocus [].
+
+Hint Extern 1 (Register focus (Sitems _)) => 
+  Provide Sitems_focus.
+Hint Extern 1 (Register unfocus (record_repr `{ nb' := _; items' := _ }')) =>  
+  Provide Sitems_unfocus.
+
+Lemma sitems_push_spec' : forall (A:Type) (r:loc) (L:list A) (x:A),
+  app sitems_push [x r] (r ~> Sitems L) (# r ~> Sitems (x::L)).
+Proof using. 
+  xcf. dup 2.
+  { xfocus r. xextract ;=> n E. skip. } 
+  { xfocusx r ;=> n E. xapps. xapps. xapps. xapp.
+    xunfocus r. rew_list; math. xsimpl~. }
+Qed.
+
+
+(********************************************************************)
+(* ** Arrays *)
+
+Require Import Array_ml Array_proof.
+
+Section Array.
+
+Hint Extern 1 (@index _ (list _) _ _ _) => apply index_bounds_impl : maths.
+Hint Extern 1 (_ < length (?l[?i:=?v])) => rewrite length_update : maths.
+Ltac auto_tilde ::= auto with maths.
+
+Lemma array_ops_spec : 
+  app array_ops [tt] \[] \[= 3].
+Proof using.
+  xcf.
+  xapp. math. => L EL. 
+  asserts LL: (length L = 3). subst. rewrite length_make; math. 
+  xapps. { apply index_bounds_impl; math. }
+  xapp~.
+  xapps~.
+  xapps~.
+  xapps~.
+  xsimpl. subst. rew_arr~. 
+Qed.
+
+End Array.
+
 
 
 

lib/coq/CFTactics.v

@@ -503,11 +503,13 @@ Ltac xok_core cont :=  (* see [xok] spec further *)
 Ltac math_0 ::= xclean. (* TODO: why needed? *)
 
 Ltac xauto_common cont :=
-  cfml_check_not_tagged tt;  
-  try solve [ cont tt 
-            | solve [ apply refl_equal ]
-            | xok_core ltac:(fun _ => solve [ cont tt | substs; cont tt ] ) 
-            | substs; if_eq; solve [ cont tt | apply refl_equal ]  ].
+  first [ 
+    cfml_check_not_tagged tt;  
+    try solve [ cont tt 
+              | solve [ apply refl_equal ]
+              | xok_core ltac:(fun _ => solve [ cont tt | substs; cont tt ] ) 
+              | substs; if_eq; solve [ cont tt | apply refl_equal ]  ]
+  | idtac ].
 
 Ltac xauto_tilde_default cont := xauto_common cont.
 Ltac xauto_star_default cont := xauto_common cont.
@@ -1108,8 +1110,14 @@ Tactic Notation "xchange" constr(E1) constr(E2) constr(E3) :=
     Then, use: [xfocus p].
     
     Variants:
+    - [xfocusx t]  is short for [xfocus t; xextract] 
+
+    - [xfocusxs t]  is short for [xfocus t; xextracts]  // EXPERIMENTAL
+
     - [xfocus2 p] to perform [xfocus p] twice. Only applies when there
-      is no existentials to be extracted after the first [xfocus]. *)
+      is no existentials to be extracted after the first [xfocus].
+
+*)
 
 Ltac get_refocus_args tt :=
   match goal with 
@@ -1143,24 +1151,6 @@ Tactic Notation "xfocus" "~" constr(t) :=
 Tactic Notation "xfocus" "*" constr(t) :=
   xfocus t; xauto*.
 
-
-(* DEPRECATED
-Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) :=
-  xfocus t; xextract as I1.
-Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2) :=
-  xfocus t; xextract as I1 I2.
-Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2)
-  simple_intropattern(I3) :=
-  xfocus t; xextract as I1 I2 I3.
-Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2)
-  simple_intropattern(I3) simple_intropattern(I4) :=
-  xfocus t; xextract as I1 I2 I3 I4.
-Tactic Notation "xfocus" constr(t) "as" simple_intropattern(I1) simple_intropattern(I2)
-  simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) :=
-  xfocus t; xextract as I1 I2 I3 I4 I5.
-*)
-
-
 Tactic Notation "xfocus2" constr(x) :=
   xfocus x; xfocus x.
 Tactic Notation "xfocus2" "~" constr(x) :=
@@ -1168,6 +1158,13 @@ Tactic Notation "xfocus2" "~" constr(x) :=
 Tactic Notation "xfocus2" "*" constr(x) :=
   xfocus2 x; xauto_star.
 
+Tactic Notation "xfocusx" constr(t) :=
+  xfocus t; xextract.
+
+Tactic Notation "xfocusxs" constr(t) :=
+  xfocus t; xextracts.
+
+
 
 (************************************************************)
 (* ** [xunfocus] *)
@@ -2560,7 +2557,7 @@ Tactic Notation "xspec" constr(f) :=
   xspec_core f.
 
 Ltac cfml_apply_xseq_or_xlet_to_reveal_app cont :=
-  match cfml_get_tag tt with
+  lazymatch cfml_get_tag tt with
   | tag_let => xlet; [ cont tt | ]
   | tag_seq => xseq; [ cont tt | ]
   | tag_apply => xuntag tag_apply; cont tt

lib/stdlib/Array_proof.v

@@ -46,7 +46,7 @@ Qed.
 
 Parameter length_spec : curried 1%nat length /\
   forall A (L:list A) (t:loc),
-  app_keep length [t] (t ~> Array L) (fun n => \[n = LibList.length L]).
+  app_keep length [t] (t ~> Array L) (fun n => \[n = LibListZ.length L]).
   
 Hint Extern 1 (RegisterSpec length) => Provide length_spec.
 
@@ -62,7 +62,7 @@ Parameter set_spec : curried 2%nat set /\
   index L i -> 
   app set [t i v] (t ~> Array L) (# t ~> Array (L[i:=v])).
   
-Hint Extern 1 (RegisterSpec get) => Provide get_spec.
+Hint Extern 1 (RegisterSpec set) => Provide set_spec.
 
 
 Notation "'App'' r `[ i ]" := (App get r i;)

lib/stdlib/List_proof.v

@@ -7,7 +7,8 @@ Require Import List_ml.
 Generalizable Variables A.
 
 
-Ltac xauto_tilde ::= unfold measure; rew_list in *; try math; auto.
+Ltac auto_tilde ::= unfold measure; rew_list in *; try math; auto.
+  (* Restored to default at the end of the file *)
 
 
 (************************************************************)
@@ -118,6 +119,7 @@ Qed. (* TODO: beautify this proof *)
 
 
 
+Ltac auto_tilde ::= auto_tilde_default.
 
 
 

lib/stdlib/Makefile

@@ -121,11 +121,13 @@ Stdlib.vio: Array_ml.vio List_ml.vio Pervasives_ml.vio
 ##############################################################
 # Coq compilation rules for %_proof.v files
 
-# Stdlib.vo: Stdlib.v Pervasives_ml.vo Array_ml.vo List_ml.vo 
+Array_ml.vo: Pervasives_ml.vo
+Array_proof.vo: Array_ml.vo
+Stdlib.vo: Stdlib.v Pervasives_ml.vo Array_ml.vo List_ml.vo 
 # 	$(COQC) $(COQINCLUDE) Stdlib.v
 #	@$(MAKE) -C $(CFML) --no-print-directory coqlib_quick  
 
-# Stdlib.vio: Stdlib.v Pervasives_ml.vio Array_ml.vio List_ml.vio
+Stdlib.vio: Stdlib.v Pervasives_ml.vio Array_ml.vio List_ml.vio
 # 	$(COQC) -quick $(COQINCLUDE) Stdlib.v
 
 #%_proof.vo: %_proof.v