Commit fc3a6a7b by Jean-Christophe Filliâtre

### example VSTTE 12 combinators completed

parent b75d15b5
 ... ... @@ -136,14 +136,17 @@ module Combinators function ks (n: int) : term axiom ksO: ks 0 = K axiom ksS: forall n: int. 0 <= n -> ks (n+1) = App (ks n) K axiom ksS: forall n: int. n >= 0 -> ks (n+1) = App (ks n) K lemma ks1: ks 1 = App K K lemma only_K_ks: forall n: int. n >= 0 -> only_K (ks n) lemma ks_inversion: forall n: int. n >= 0 -> n = 0 \/ n > 0 /\ ks n = App (ks (n-1)) K n = 0 \/ n > 0 /\ ks n = App (ks (n-1)) K lemma ks_injective: forall n1 n2: int. n1 >= 0 -> n2 >= 0 -> ks n1 = ks n2 -> n1 = n2 use import int.EuclideanDivision ... ... @@ -163,7 +166,8 @@ module Combinators end end { is_value result /\ forall n: int. n >= 0 -> t = ks n -> result = ks (mod n 2) } forall n: int. n >= 0 -> (t = ks (2*n) -> result = K) /\ (t = ks (2*n+1) -> result = App K K) } lemma ks_value: forall n: int. 0 <= n -> is_value (ks n) -> 0 <= n <= 1 ... ...
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. Require int.Abs. Require int.EuclideanDivision. (* Why3 assumption *) Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. (* Why3 assumption *) Inductive term := | S : term | K : term | App : term -> term -> term . (* Why3 assumption *) Set Implicit Arguments. 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. Unset Implicit Arguments. (* Why3 assumption *) Inductive context := | Hole : context | Left : context -> term -> context | Right : term -> context -> context . (* Why3 assumption *) Set Implicit Arguments. 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. Unset Implicit Arguments. (* Why3 assumption *) Set Implicit Arguments. 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. Unset Implicit Arguments. (* 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))). Axiom reducible_or_value : forall (t:term), (exists tqt:term, (infix_mnmngt t tqt)) \/ (is_value t). (* Why3 assumption *) Definition irreducible(t:term): Prop := forall (tqt:term), ~ (infix_mnmngt t tqt). Axiom irreducible_is_value : forall (t:term), (irreducible t) <-> (is_value t). (* Why3 assumption *) Inductive only_K : term -> Prop := | only_K_K : (only_K K) | only_K_App : forall (t1:term) (t2:term), (only_K t1) -> ((only_K t2) -> (only_K (App t1 t2))). Axiom only_K_reduces : forall (t:term), (only_K t) -> exists v:term, (relTR t v) /\ ((is_value v) /\ (only_K v)). (* Why3 assumption *) Set Implicit Arguments. Fixpoint size(t:term) {struct t}: Z := match t with | (K|S) => 0%Z | (App t1 t2) => ((1%Z + (size t1))%Z + (size t2))%Z end. Unset Implicit Arguments. Axiom size_nonneg : forall (t:term), (0%Z <= (size t))%Z. Parameter ks: Z -> term. Axiom ksO : ((ks 0%Z) = K). Axiom ksS : forall (n:Z), (0%Z <= n)%Z -> ((ks (n + 1%Z)%Z) = (App (ks n) K)). Axiom ks1 : ((ks 1%Z) = (App K K)). Axiom only_K_ks : forall (n:Z), (0%Z <= n)%Z -> (only_K (ks n)). Axiom ks_inversion : forall (n:Z), (0%Z <= n)%Z -> ((n = 0%Z) \/ ((0%Z < n)%Z /\ ((ks n) = (App (ks (n - 1%Z)%Z) K)))). Axiom ks_injective : forall (n1:Z) (n2:Z), (0%Z <= n1)%Z -> ((0%Z <= n2)%Z -> (((ks n1) = (ks n2)) -> (n1 = n2))). Require Import Why3. Ltac ae := why3 "alt-ergo". Lemma mod_0_2: (EuclideanDivision.mod1 0 2 = 0)%Z. generalize (EuclideanDivision.Div_mod 0 2). generalize (EuclideanDivision.Mod_bound 0 2). rewrite Zabs_eq; ae. Qed. (* Why3 goal *) Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z, (0%Z <= n)%Z /\ (t = (ks n))) -> match t with | S => True | K => True | (App t1 t2) => (exists n:Z, (0%Z <= n)%Z /\ (t1 = (ks n))) -> forall (result:term), ((is_value result) /\ forall (n:Z), (0%Z <= n)%Z -> (((t1 = (ks (2%Z * n)%Z)) -> (result = K)) /\ ((t1 = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> (result = (App K K))))) -> match result with | K => (exists n:Z, (0%Z <= n)%Z /\ (t2 = (ks n))) -> forall (result1:term), ((is_value result1) /\ forall (n:Z), (0%Z <= n)%Z -> (((t2 = (ks (2%Z * n)%Z)) -> (result1 = K)) /\ ((t2 = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> (result1 = (App K K))))) -> forall (n:Z), (0%Z <= n)%Z -> ((t = (ks (2%Z * n)%Z)) -> ((App K result1) = K)) | S => True | (App K v1) => True | (App S v1) => True | (App (App S v1) v2) => True | _ => True end end. intros t (n, (h1, h2)). destruct t; auto. intros (n1, (h3, h4)). destruct result as [] _eqn. intuition. intros (h5, h6) (n2, (h7, h8)). intros res1 (h9, h10). intros n0 hn0 eq0. generalize (h10 n2 h7); clear h10; intros ht2. assert (n2 = 0)%Z. generalize (ks_inversion n2 h7). intuition. generalize (ks_inversion n h1). ae. assert (h: (0 <= 2*n0)%Z) by ae. generalize (ks_inversion (2*n0)%Z h). intuition. ae. assert (t1 = ks (2*(n0-1)+1))%Z by ae. assert (n1 = 2 * (n0 - 1) + 1)%Z by ae. ae. destruct t3; auto. destruct t3_1; auto. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. Require int.Abs. Require int.EuclideanDivision. (* Why3 assumption *) Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. (* Why3 assumption *) Inductive term := | S : term | K : term | App : term -> term -> term . (* Why3 assumption *) Set Implicit Arguments. 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. Unset Implicit Arguments. (* Why3 assumption *) Inductive context := | Hole : context | Left : context -> term -> context | Right : term -> context -> context . (* Why3 assumption *) Set Implicit Arguments. 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. Unset Implicit Arguments. (* Why3 assumption *) Set Implicit Arguments. 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. Unset Implicit Arguments. (* 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))). Axiom reducible_or_value : forall (t:term), (exists tqt:term, (infix_mnmngt t tqt)) \/ (is_value t). (* Why3 assumption *) Definition irreducible(t:term): Prop := forall (tqt:term), ~ (infix_mnmngt t tqt). Axiom irreducible_is_value : forall (t:term), (irreducible t) <-> (is_value t). (* Why3 assumption *) Inductive only_K : term -> Prop := | only_K_K : (only_K K) | only_K_App : forall (t1:term) (t2:term), (only_K t1) -> ((only_K t2) -> (only_K (App t1 t2))). Axiom only_K_reduces : forall (t:term), (only_K t) -> exists v:term, (relTR t v) /\ ((is_value v) /\ (only_K v)). (* Why3 assumption *) Set Implicit Arguments. Fixpoint size(t:term) {struct t}: Z := match t with | (K|S) => 0%Z | (App t1 t2) => ((1%Z + (size t1))%Z + (size t2))%Z end. Unset Implicit Arguments. Axiom size_nonneg : forall (t:term), (0%Z <= (size t))%Z. Parameter ks: Z -> term. Axiom ksO : ((ks 0%Z) = K). Axiom ksS : forall (n:Z), (0%Z <= n)%Z -> ((ks (n + 1%Z)%Z) = (App (ks n) K)). Axiom ks1 : ((ks 1%Z) = (App K K)). Axiom only_K_ks : forall (n:Z), (0%Z <= n)%Z -> (only_K (ks n)). Axiom ks_inversion : forall (n:Z), (0%Z <= n)%Z -> ((n = 0%Z) \/ ((0%Z < n)%Z /\ ((ks n) = (App (ks (n - 1%Z)%Z) K)))). Axiom ks_injective : forall (n1:Z) (n2:Z), (0%Z <= n1)%Z -> ((0%Z <= n2)%Z -> (((ks n1) = (ks n2)) -> (n1 = n2))). Require Import Why3. Ltac ae := why3 "alt-ergo". Require Import int.EuclideanDivision. Lemma div2: forall n: Z, (0 <= n)%Z -> (exists n': Z, 0 <= n' /\ n = 2 * n')%Z \/ (exists n': Z, 0 <= n' /\ n = 2 * n' + 1)%Z. intros n hn. generalize (Div_mod n 2). generalize (Mod_bound n 2). intuition. assert (e: (Zabs 2 = 2)%Z) by (simpl; auto). rewrite e in H2. assert (mod1 n 2 = 0 \/ mod1 n 2 = 1)%Z by omega. destruct H0. left; exists (div n 2); ae. right; exists (div n 2); ae. Qed. (* Why3 goal *) Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z, (0%Z <= n)%Z /\ (t = (ks n))) -> match t with | S => True | K => True | (App t1 t2) => (exists n:Z, (0%Z <= n)%Z /\ (t1 = (ks n))) -> forall (result:term), ((is_value result) /\ forall (n:Z), (0%Z <= n)%Z -> (((t1 = (ks (2%Z * n)%Z)) -> (result = K)) /\ ((t1 = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> (result = (App K K))))) -> match result with | K => (exists n:Z, (0%Z <= n)%Z /\ (t2 = (ks n))) -> forall (result1:term), ((is_value result1) /\ forall (n:Z), (0%Z <= n)%Z -> (((t2 = (ks (2%Z * n)%Z)) -> (result1 = K)) /\ ((t2 = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> (result1 = (App K K))))) -> forall (n:Z), (0%Z <= n)%Z -> ((t = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> ((App K result1) = (App K K))) | S => True | (App K v1) => True | (App S v1) => True | (App (App S v1) v2) => True | _ => True end end. intros t (n, (h1, h2)). destruct t; auto. intros (n1, (h3, h4)). destruct result; auto. intros (_, ht1). intros (n2, (h5,h6)). assert (n2 = 0)%Z. destruct (ks_inversion n h1); ae. destruct result1; auto. intros (_, ht2). destruct (div2 n2 h5) as [(n',h')|(n',h')]. ae. ae. intros (_, ht2). generalize (ht2 n2 h5); intuition. ae. destruct result1; auto. destruct result1_1; auto. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. Require int.Abs. Require int.EuclideanDivision. (* Why3 assumption *) Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. (* Why3 assumption *) Inductive term := | S : term | K : term | App : term -> term -> term . (* Why3 assumption *) Set Implicit Arguments. 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. Unset Implicit Arguments. (* Why3 assumption *) Inductive context := | Hole : context | Left : context -> term -> context | Right : term -> context -> context . (* Why3 assumption *) Set Implicit Arguments. 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. Unset Implicit Arguments. (* Why3 assumption *) Set Implicit Arguments. 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. Unset Implicit Arguments. (* 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)