Commit 4230f744 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new example vstte12_combinators (in progress)

parent 58a5daa2
(* The 2nd Verified Software Competition (VSTTE 2012)
https://sites.google.com/site/vstte2012/compet
Problem 2:
Combinators S and K *)
module Combinators
type term = S | K | App term term
(* specification of the CBV reduction *)
predicate is_value (t: term) = 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
(* contexts *)
type context = Hole | Left context term | Right term context
predicate is_context (c: context) = match c with
| Hole -> true
| Left c _ -> is_context c
| Right v c -> is_value v && is_context c
end
function subst (c: context) (t: term) : term = match c with
| Hole -> t
| Left c1 t2 -> App (subst c1 t) t2
| Right v1 c2 -> App v1 (subst c2 t)
end
(* one step reduction
(the notion of context is inlined in the following definition) *)
inductive (-->) (t1 t2: term) =
| red_K:
forall c: context. is_context c ->
forall v1 v2: term. is_value v1 -> is_value v2 ->
subst c (App (App K v1) v2) --> subst c v1
| red_S:
forall c: context. is_context c ->
forall v1 v2 v3: term. is_value v1 -> is_value v2 -> is_value v3 ->
subst c (App (App (App S v1) v2) v3) -->
subst c (App (App v1 v3) (App v2 v3))
lemma red_left:
forall t1 t2 t: term. t1 --> t2 -> App t1 t --> App t2 t
lemma red_right:
forall v t1 t2: term. is_value v -> t1 --> t2 -> App v t1 --> App v t2
clone import relations.ReflTransClosure
with type t = term, predicate rel = (-->)
predicate (-->*) (t1 t2: term) = relTR t1 t2
lemma red_star_left:
forall t1 t2 t: term. t1 -->* t2 -> App t1 t -->* App t2 t
lemma red_star_right:
forall v t1 t2: term. is_value v -> t1 -->* t2 -> App v t1 -->* App v t2
(* task 1: implement CBV reduction *)
let rec reduction (t: term) : term =
{}
match t with
| S -> S
| K -> K
| App t1 t2 -> match reduction t1 with
| K -> App K (reduction t2)
| S -> App S (reduction t2)
| App K v1 -> let _ = reduction t2 in v1
| App S v1 -> App (App S v1) (reduction t2)
| App (App S v1) v2 ->
let v3 = reduction t2 in reduction (App (App v1 v3) (App v2 v3))
| _ -> absurd
end
end
{ t-->*result /\ is_value result }
(* an irreducible term is a value *)
lemma reducible_or_value:
forall t: term. (exists t': term. t-->t') \/ is_value t
predicate irreducible (t: term) = forall t': term. not (t-->t')
lemma irreducible_is_value:
forall t: term. irreducible t <-> is_value t
(* task 2 *)
use import int.Int
inductive only_K (t: term) =
| only_K_K:
only_K K
| only_K_App:
forall t1 t2: term. only_K t1 -> only_K t2 -> only_K (App t1 t2)
lemma only_K_reduces:
forall t: term. only_K t ->
exists v: term. t -->* v /\ is_value v /\ only_K v
function size (t: term) : int = match t with
| K | S -> 0
| App t1 t2 -> 1 + size t1 + size t2
end
lemma size_nonneg: forall t: term. size t >= 0
let rec reduction2 (t: term) : term variant { size t } =
{ only_K t }
match t with
| S -> S
| K -> K
| App t1 t2 -> match reduction2 t1 with
| K -> App K (reduction2 t2)
| S -> App S (reduction2 t2)
| App K v1 -> let _ = reduction2 t2 in v1
| App S v1 -> App (App S v1) (reduction2 t2)
| App (App S v1) v2 ->
let v3 = reduction2 t2 in reduction2 (App (App v1 v3) (App v2 v3))
| _ -> absurd
end
end
{ only_K result /\ is_value result }
(* task 3 *)
function ks (n: int) : term
axiom ksO: ks 0 = K
axiom ksS: forall n: int. 0 <= n -> 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
use import int.EuclideanDivision
let rec reduction3 (t: term) : term =
{ exists n: int. n >= 0 /\ t = ks n }
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))
| _ -> absurd
end
end
{ is_value result /\
forall n: int. n >= 0 -> t = ks n -> result = ks (mod n 2) }
lemma ks_value:
forall n: int. 0 <= n -> is_value (ks n) -> 0 <= n <= 1
lemma ks_even_odd:
forall n: int. 0 <= n -> ks (2*n) -->* K
/\ ks (2*n+1) -->* App K K
end
(*
Local Variables:
compile-command: "why3ide vstte12_combinators.mlw"
End:
*)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.
(* 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.
(* Why3 goal *)
Theorem WP_parameter_reduction2 : forall (t:term), (only_K t) ->
match t with
| S => True
| K => True
| (App t1 t2) => (((0%Z <= (size t))%Z /\ ((size t1) < (size t))%Z) /\
(only_K t1)) -> forall (result:term), ((only_K result) /\
(is_value result)) ->
match result with
| K => True
| S => True
| (App K v1) => True
| (App S v1) => True
| (App (App S v1) v2) => (((0%Z <= (size t))%Z /\
((size t2) < (size t))%Z) /\ (only_K t2)) ->
forall (result1:term), ((only_K result1) /\ (is_value result1)) ->
((size (App (App v1 result1) (App v2 result1))) < (size t))%Z
| _ => True
end
end.
intuition.
destruct t; intuition.
destruct result; intuition.
destruct result1; intuition.
destruct result1_1; intuition.
inversion H4.
inversion H12.
inversion H16.
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.
(* 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.
(* Why3 goal *)
Theorem WP_parameter_reduction2 : forall (t:term), (only_K t) ->
match t with
| S => True
| K => True
| (App t1 t2) => (((0%Z <= (size t))%Z /\ ((size t1) < (size t))%Z) /\
(only_K t1)) -> forall (result:term), ((only_K result) /\
(is_value result)) ->
match result with
| K => True
| S => True
| (App K v1) => True
| (App S v1) => True
| (App (App S v1) v2) => (((0%Z <= (size t))%Z /\
((size t2) < (size t))%Z) /\ (only_K t2)) ->
forall (result1:term), ((only_K result1) /\ (is_value result1)) ->
(only_K (App (App v1 result1) (App v2 result1)))
| _ => True
end
end.
intuition.
destruct t; intuition.
destruct result; intuition.
destruct result1; intuition.
destruct result1_1; intuition.
inversion H4.
inversion H12.
inversion H16.
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 *)