Commit 506e9b84 by charguer

### recfun

parent 34f4e43f
 ... @@ -485,7 +485,7 @@ let for_incr () = ... @@ -485,7 +485,7 @@ let for_incr () = let rec rec_partial_half x = let rec rec_partial_half x = if x = 0 then 0 if x = 0 then 0 else if x = 1 then assert false else if x = 1 then assert false else 1 + rec_partial_half(x-2) else 1 + rec_partial_half (x-2) let rec rec_mutual_f x = let rec rec_mutual_f x = if x <= 0 then x else 1 + rec_mutual_g (x-2) if x <= 0 then x else 1 + rec_mutual_g (x-2) ... ...
 ... @@ -29,6 +29,12 @@ Tactic Notation "xrets" "*" constr(Q) := ... @@ -29,6 +29,12 @@ Tactic Notation "xrets" "*" constr(Q) := (********************************************************************) (********************************************************************) (********************************************************************) (********************************************************************) (********************************************************************) (********************************************************************) ... @@ -664,6 +670,48 @@ let order_record () = ... @@ -664,6 +670,48 @@ let order_record () = *) *) (********************************************************************) (* ** Recursive function *) Require Import LibInt. Lemma rec_partial_half_spec : forall x n, n = 2 * x -> app rec_partial_half [n] \[] \[= x]. Proof using. => x. induction_wf IH: (downto 0) x. xcf. xif. { xrets~. } { xif. { xfail. math. } { xapps (x-1). { unfolds. skip. (* TODO Anomaly: Z.sub is not an evaluable constant. => maybe because I made it opaque? *) } { skip. } { xrets. skip. } } } Qed. Lemma rec_mutual_f_and_g_spec : (forall (x:int), x >= 0 -> app rec_mutual_f [x] \[] \[= x]) /\ (forall (x:int), x >= -1 -> app rec_mutual_g [x] \[] \[= x+1]). Proof using. intros. cuts G: (forall (m:int), (forall x, x <= m -> x >= 0 -> app rec_mutual_f [x] \[] \[= x]) /\ (forall x, x+1 <= m -> x >= -1 -> app rec_mutual_g [x] \[] \[= x+1])). { split; intros x P; specializes G (x+1); destruct G as [G1 G2]; xapp~. } => m. induction_wf IH: (downto 0) m. split; intros x Lx Px. { xcf. xif. xrets~. xapp (x-1). unfolds. skip. (* TODO *) skip. skip. intro_subst. xrets. skip. } { xcf. xapp x. unfolds. skip. (* TODO *) skip. skip. } Qed. ... @@ -856,25 +904,6 @@ Proof using. ... @@ -856,25 +904,6 @@ Proof using. Qed. Qed. (********************************************************************) (* ** Recursive function *) Lemma rec rec_partial_half x = if x = 0 then 0 else if x = 1 then assert false else 1 + rec_partial_half(x-2) Proof using. xcf. Qed. let rec rec_mutual_f x = if x <= 0 then x else 1 + rec_mutual_g (x-2) and rec rec_mutual g x = rec_mutual_f (x+1) *) (* TODO: include demo of xpost (fun r =>\[r = 3]). *) (* TODO: include demo of xpost (fun r =>\[r = 3]). *) ... @@ -884,63 +913,6 @@ and rec rec_mutual g x = ... @@ -884,63 +913,6 @@ and rec rec_mutual g x = (*************************************************************************) (*************************************************************************) (*************************************************************************) (*************************************************************************) (*************************************************************************) (** * Polymorphic let demos (** Demo top-level polymorphic let. *) Lemma poly_top_spec : forall A, poly_top = @nil A. Proof using. xcf. Qed. (** Demo local polymorphic let. *) Lemma poly_let_1_spec : forall A, Spec poly_let_1 () |B>> B \[] (fun (x:list A) => \[x = nil]). Proof using. xcf. xval. subst. xrets. auto. Qed. (** Demo [xval_st P] *) Lemma poly_let_1_spec' : forall A, Spec poly_let_1 () |B>> B \[] (fun (x:list A) => \[x = nil]). Proof using. xcf. xval_st (fun a => a = @nil). extens~. xrets. subst~. Qed. (** Demo [xval_st P as x Hx] *) Lemma poly_let_1_spec'' : forall A, Spec poly_let_1 () |B>> B \[] (fun (x:list A) => \[x = nil]). Proof using. xcf. xval_st (fun a => a = @nil) as p Hp. extens~. xrets. subst~. Qed. (** Demo for partially-polymorphic values. *) Lemma poly_let_2_spec : forall A1 A2, Spec poly_let_2 () |B>> B \[] (fun '(x,y) : list A1 * list A2 => \[x = nil /\ y = nil]). Proof using. intros. xcf. xvals. xrets. auto. Qed. Lemma poly_let_2_same_spec : forall A, Spec poly_let_2_same () |B>> B \[] (fun '(x,y) : list A * list A => \[x = nil /\ y = nil]). Proof using. intros. xcf. xvals. xrets. auto. Qed. Lemma poly_let_2_partial_spec : forall A, Spec poly_let_2_partial () |B>> B \[] (fun '(x,y) : list A * list int => \[x = nil /\ y = nil]). Proof using. intros. xcf. xval as p Hp. subst p. xrets. auto. Qed. *) (* let (top_val_pair_int_1,top_val_pair_int_2) = (1,2) let (top_val_pair_fun_1,top_val_pair_fun_2) = (fun x -> x), (fun x -> x) *) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!