Commit c1fc50f7 authored by Martin Clochard's avatar Martin Clochard
Browse files

removing coq tactic from vstte12_combinators example

parent b0b70223
......@@ -57,37 +57,40 @@ module Combinators
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
type zipper = ZHole | ZLeft context term | ZRight term context
let rec function subst_c (c ct:context) : context
ensures { is_context c /\ is_context ct -> is_context result }
= match c with
| Hole -> ct
| Left c1 t2 -> Left (subst_c c1 ct) t2
| Right v1 c2 -> Right v1 (subst_c c2 ct)
end
lemma red_star_right:
forall v t1 t2: term. is_value v -> t1 -->* t2 -> App v t1 -->* App v t2
lemma subst_c_commute : forall c [@induction] ct t.
subst c (subst ct t) = subst (subst_c c ct) t
(* task 1: implement CBV reduction *)
let rec reduction (t: term) : term
let rec reduction (ghost c:context) (t: term) : term
diverges (* there are non-normalizable terms... *)
ensures { t -->* result /\ is_value result }
requires { is_context c }
ensures { subst c t -->* subst c result }
ensures { is_value result }
= 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))
| App t1 t2 ->
let v1 = reduction (subst_c c (Left Hole t2)) t1 in
let v2 = reduction (subst_c c (Right v1 Hole)) t2 in
match v1 with
| K | S | App S _ -> App v1 v2
| App K v3 -> v3
| App (App S v3) v4 -> reduction c (App (App v3 v2) (App v4 v2))
| _ -> absurd
end
end
......@@ -99,21 +102,46 @@ module Combinators
let test_SKK ()
diverges (* would be hard to prove terminating *)
raises { BenchFailure -> true }
= let t1 = reduction (App i i) in
= let t1 = reduction Hole (App i i) in
if not (eq t1 i) then raise BenchFailure;
let t2 = reduction (App (App (App (App K K) K) K) K) in
let t2 = reduction Hole (App (App (App (App K K) K) K) K) in
if not (eq t2 K) then raise BenchFailure;
t1, t2
(* an irreducible term is a value *)
predicate irreducible (t: term) = forall t': term. not (t-->t')
lemma reducible_or_value:
forall t: term. (exists t': term. t-->t') \/ is_value t
exception Fail
let rec ghost reduce_step (c:context) (t:term) : term
requires { is_context c }
ensures { subst c t --> subst c result }
raises { Fail -> is_value t }
variant { t }
= match t with
| App t1 t2 ->
try App (reduce_step (subst_c c (Left Hole t2)) t1) t2 with Fail ->
try App t1 (reduce_step (subst_c c (Right t1 Hole)) t2) with Fail ->
match t1 with
| App K v -> v
| App (App S v1) v2 -> App (App v1 t2) (App v2 t2)
| _ -> raise Fail
end end end
| _ -> raise Fail
end
predicate irreducible (t: term) = forall t': term. not (t-->t')
let rec lemma value_in_context (c:context) (t:term) : unit
requires { is_value (subst c t) }
ensures { is_value t }
variant { c }
= match c with
| Hole -> ()
| Left cl _ -> value_in_context cl t
| Right _ cr -> value_in_context cr t
end
lemma irreducible_is_value:
forall t: term. irreducible t <-> is_value t
let lemma irreducible_is_value (t:term) : unit
ensures { irreducible t <-> is_value t }
= try let _ = reduce_step Hole t in () with Fail -> () end
(* task 2 *)
......@@ -125,76 +153,60 @@ module Combinators
| 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 { t }
requires { only_K t }
let rec reduction2 (ghost c:context) (t: term) : term
requires { only_K t /\ is_context c }
ensures { only_K result /\ is_value result }
ensures { subst c t -->* subst c result }
variant { 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))
| App t1 t2 ->
let v1 = reduction2 (subst_c c (Left Hole t2)) t1 in
let v2 = reduction2 (subst_c c (Right v1 Hole)) t2 in
match v1 with
| K -> App v1 v2
| App K v3 -> v3
| _ -> absurd
end
| _ -> absurd
end
(* task 3 *)
let rec function ks (n: int) : term
requires { n >= 0 }
ensures { only_K result }
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)
lemma ks_inversion: forall n: int. n >= 0 ->
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 number.Parity
let rec reduction3 (t: term) (ghost n:int) : term
requires { n >= 0 /\ t = ks n }
let rec reduction3 (ghost c:context) (ghost n:int) (t: term) : term
requires { n >= 0 /\ t = ks n /\ is_context c }
variant { n }
ensures { subst c t -->* subst c result }
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 _ -> match reduction3 t1 (n-1) with
| K -> App K K
| App K K -> K
| App t1 t2 ->
let v1 = reduction3 (subst_c c (Left Hole t2)) (n-1) t1 in
let v2 = reduction3 (subst_c c (Right v1 Hole)) 0 t2 in
match v1 with
| K -> App v1 v2
| App K v3 -> v3
| _ -> absurd
end
| _ -> absurd
end
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
let lemma ks_even_odd (n:int) : unit
requires { n >= 0 }
ensures { ks (2*n) -->* K }
ensures { ks (2*n+1) -->* App K K }
= let _ = reduction3 Hole (2*n) (ks (2*n)) in
let _ = reduction3 Hole (2*n+1) (ks (2*n+1)) in
()
end
(* 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.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive term :=
| S : term
| K : term
| App : term -> term -> term.
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* 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))).
Axiom reducible_or_value : forall (t:term), (exists t':term, (infix_mnmngt t
t')) \/ (is_value t).
(* Why3 assumption *)
Definition irreducible (t:term): Prop := forall (t':term), ~ (infix_mnmngt t
t').
Hint Constructors infix_mnmngt.
Hint Unfold is_value.
Require Import Why3.
Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 5; admit.
(* Why3 goal *)
Theorem irreducible_is_value : forall (t:term), (irreducible t) <-> (is_value
t).
(* Why3 intros t. *)
split.
destruct (reducible_or_value t).
destruct H as (t',h').
intro.
elim H with t'; auto.
auto.
(* is_value -> irreducible *)
induction t; intuition.
red; intros t' ht'.
inversion ht'.
destruct c; simpl in H0; ae.
destruct c; simpl in H0; ae.
(* irreducible K *)
red; intros t' ht'.
inversion ht'.
destruct c; simpl in H0; ae.
destruct c; simpl in H0; ae.
(* irreducible (App t1 t2) *)
red; intros t' ht'.
inversion ht'.
assert (forall c: context, ~ (is_value (subst c (App (App K v1) v2)))).
induction c0; auto.
simpl.
destruct c0; simpl.
intuition.
destruct c0; simpl; intuition.
destruct t0; simpl; intuition.
destruct t; simpl; intuition.
destruct t3; ae.
ae.
assert (forall c: context, ~ (is_value (subst c (App (App (App S v1) v2) v3)))).
induction c0; simpl; intuition.
destruct c0; simpl; intuition.
destruct c0; simpl; intuition.
destruct t0; simpl; intuition.
ae.
destruct t; simpl; intuition.
destruct t3; ae.
ae.
Admitted.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require number.Parity.
(* 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))).
Axiom reducible_or_value : forall (t:term), (exists t':term, (infix_mnmngt t
t')) \/ (is_value t).
(* Why3 assumption *)
Definition irreducible (t:term): Prop := forall (t':term), ~ (infix_mnmngt t
t').
Axiom irreducible_is_value : forall (t:term), (irreducible t) <-> (is_value
t).