ported example vstte12_combinators

bench/bench

@@ -227,7 +227,7 @@ execute examples/fibonacci.mlw FibonacciLogarithmic.bench
 # fails: cannot evaluate condition a=b (how to do it?)
 # execute examples/same_fringe.mlw SameFringe.test5
 execute examples/same_fringe.mlw Test.test1
-execute examples/to_port/vstte12_combinators.mlw Combinators.test_SKK
+execute examples/vstte12_combinators.mlw Combinators.test_SKK
 execute examples/selection_sort.mlw SelectionSort.bench
 execute examples/insertion_sort.mlw InsertionSort.bench
 execute examples/quicksort.mlw Test.bench

examples/to_port/vstte12_combinators.mlw → examples/vstte12_combinators.mlw

@@ -155,12 +155,14 @@ module Combinators
 
   (* task 3 *)
 
-  function ks (n: int) : term
-
-  axiom ksO: ks 0 = K
-  axiom ksS: forall n: int. n >= 0 -> ks (n+1) = App (ks n) K
+  let rec function ks (n: int) : term
+    requires { n >= 0 }
+    variant { n }
+  = if n = 0 then K else App (ks (n-1)) K
 
+  lemma ks0: ks 0 = K
   lemma ks1: ks 1 = App K K
+  lemma ksS: forall n. n >= 0 -> ks (n+1) = App (ks n) K
 
   lemma only_K_ks: forall n: int. n >= 0 -> only_K (ks n)
 
@@ -170,24 +172,20 @@ module Combinators
   lemma ks_injective:
     forall n1 n2: int. n1 >= 0 -> n2 >= 0 -> ks n1 = ks n2 -> n1 = n2
 
-  use import int.Div2
+  use import number.Parity
 
-  let rec reduction3 (t: term) : term
-    requires { exists n: int. n >= 0 /\ t = ks n }
-    diverges (* TODO: prove termination ... *)
-    ensures { is_value result /\
-      forall n: int. n >= 0 -> (t = ks (2*n)   -> result = K)
-                            /\ (t = ks (2*n+1) -> result = App K K) }
+  let rec reduction3 (t: term) (ghost n:int) : term
+    requires { n >= 0 /\ t = ks n }
+    variant { n }
+    ensures { is_value result }
+    ensures { even n -> result = K }
+    ensures { odd n -> result = App K K }
   = match t with
     | S -> S
     | K -> K
-    | App t1 t2 -> match reduction3 t1 with
-      | K -> App K (reduction3 t2)
-      | S -> App S (reduction3 t2)
-      | App K v1 -> let _ = reduction3 t2 in v1
-      | App S v1 -> App (App S v1) (reduction3 t2)
-      | App (App S v1) v2 ->
-          let v3 = reduction3 t2 in reduction3 (App (App v1 v3) (App v2 v3))
+    | App t1 _ -> match reduction3 t1 (n-1) with
+      | K -> App K K
+      | App K K -> K
       | _ -> absurd
       end
     end

examples/vstte12_combinators/vstte12_combinators_Combinators_VC_reduction_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+
+(* Why3 assumption *)
+Inductive term :=
+  | S : term
+  | K : term
+  | App : term -> term -> term.
+Axiom term_WhyType : WhyType term.
+Existing Instance term_WhyType.
+
+Parameter eq: term -> term -> Prop.
+
+Axiom eq_def : forall (x:term) (y:term), match (x,
+  y) with
+  | (S, S) => (eq x y)
+  | (K, K) => (eq x y)
+  | ((App x1 x2), (App y1 y2)) => (eq x y) <-> ((eq x1 y1) /\ (eq x2 y2))
+  | (_, _) => ~ (eq x y)
+  end.
+
+Axiom eq_spec : forall (x:term) (y:term), (eq x y) <-> (x = y).
+
+(* Why3 assumption *)
+Fixpoint is_value (t:term) {struct t}: Prop :=
+  match t with
+  | (K|S) => True
+  | ((App K v)|(App S v)) => (is_value v)
+  | (App (App S v1) v2) => (is_value v1) /\ (is_value v2)
+  | _ => False
+  end.
+
+(* Why3 assumption *)
+Inductive context :=
+  | Hole : context
+  | Left : context -> term -> context
+  | Right : term -> context -> context.
+Axiom context_WhyType : WhyType context.
+Existing Instance context_WhyType.
+
+(* Why3 assumption *)
+Fixpoint is_context (c:context) {struct c}: Prop :=
+  match c with
+  | Hole => True
+  | (Left c1 _) => (is_context c1)
+  | (Right v c1) => (is_value v) /\ (is_context c1)
+  end.
+
+(* Why3 assumption *)
+Fixpoint subst (c:context) (t:term) {struct c}: term :=
+  match c with
+  | Hole => t
+  | (Left c1 t2) => (App (subst c1 t) t2)
+  | (Right v1 c2) => (App v1 (subst c2 t))
+  end.
+
+(* Why3 assumption *)
+Inductive infix_mnmngt: term -> term -> Prop :=
+  | red_K : forall (c:context), (is_context c) -> forall (v1:term) (v2:term),
+      (is_value v1) -> ((is_value v2) -> (infix_mnmngt (subst c (App (App K
+      v1) v2)) (subst c v1)))
+  | red_S : forall (c:context), (is_context c) -> forall (v1:term) (v2:term)
+      (v3:term), (is_value v1) -> ((is_value v2) -> ((is_value v3) ->
+      (infix_mnmngt (subst c (App (App (App S v1) v2) v3)) (subst c
+      (App (App v1 v3) (App v2 v3)))))).
+
+Axiom red_left : forall (t1:term) (t2:term) (t:term), (infix_mnmngt t1 t2) ->
+  (infix_mnmngt (App t1 t) (App t2 t)).
+
+Axiom red_right : forall (v:term) (t1:term) (t2:term), (is_value v) ->
+  ((infix_mnmngt t1 t2) -> (infix_mnmngt (App v t1) (App v t2))).
+
+(* Why3 assumption *)
+Inductive relTR: term -> term -> Prop :=
+  | BaseTransRefl : forall (x:term), (relTR x x)
+  | StepTransRefl : forall (x:term) (y:term) (z:term), (relTR x y) ->
+      ((infix_mnmngt y z) -> (relTR x z)).
+
+Axiom relTR_transitive : forall (x:term) (y:term) (z:term), (relTR x y) ->
+  ((relTR y z) -> (relTR x z)).
+
+Axiom red_star_left : forall (t1:term) (t2:term) (t:term), (relTR t1 t2) ->
+  (relTR (App t1 t) (App t2 t)).
+
+Axiom red_star_right : forall (v:term) (t1:term) (t2:term), (is_value v) ->
+  ((relTR t1 t2) -> (relTR (App v t1) (App v t2))).
+
+(* Why3 goal *)
+Theorem VC_reduction : forall (t:term), forall (x:term) (x1:term),
+  (t = (App x x1)) -> forall (o:term), ((relTR x o) /\ (is_value o)) ->
+  forall (x2:term) (x3:term), (o = (App x2 x3)) -> forall (x4:term)
+  (x5:term), (x2 = (App x4 x5)) -> ((x4 = S) -> forall (v3:term), ((relTR x1
+  v3) /\ (is_value v3)) -> forall (result:term), ((relTR (App (App x5 v3)
+  (App x3 v3)) result) /\ (is_value result)) -> (relTR t result)).
+intros t x x1 h1 o (h2,h3) x2 x3 h4 x4 x5 h5 h6 v3 (h7,h8) result (h9,h10).
+subst.
+eapply relTR_transitive.
+eapply red_star_left; eauto.
+eapply relTR_transitive.
+eapply red_star_right; eauto.
+eapply relTR_transitive.
+eapply StepTransRefl.
+eapply BaseTransRefl.
+apply (red_S Hole); simpl; auto.
+inversion h3; auto.
+inversion h3; auto.
+now simpl.
+Qed.
+