Commit 426b7890 authored by Jean-Christophe's avatar Jean-Christophe
Browse files

relabel example: Coq proof for one VC

still needs a little bit of cleaning
parent a373d4fe
......@@ -4,6 +4,11 @@ module Relabel
use import list.Mem
use import list.Append
(* should be moved to the library *)
lemma mem_append :
forall x : 'a, l1 l2 : list 'a.
mem x (l1 ++ l2) <-> mem x l1 or mem x l2
type tree 'a =
| Leaf 'a
| Node (tree 'a) (tree 'a)
......@@ -29,6 +34,7 @@ module Relabel
same_shape l1 l2 -> same_shape r1 r2 ->
same_shape (Node l1 r1) (Node l2 r2)
(* should be in the library? *)
inductive distinct (l : list 'a) =
| distinct_zero : distinct (Nil : list 'a)
| distinct_one : forall x:'a. distinct (Cons x Nil)
......@@ -36,6 +42,11 @@ module Relabel
forall x :'a, l : list 'a.
not (mem x l) -> distinct l -> distinct (Cons x l)
lemma distinct_append :
forall l1 l2 : list 'a.
distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) ->
distinct (l1 ++ l2)
use import int.Int
use import module stdlib.Ref
......@@ -49,7 +60,7 @@ module Relabel
| Leaf _ -> Leaf (fresh ())
| Node l r -> Node (relabel l) (relabel r)
end
{ (* same_shape t result and *) distinct (labels result) and
{ same_shape t result and distinct (labels result) and
old r <= r and (forall x:int. mem x (labels result) -> old r < x <= r) }
end
......
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter ghost : forall (a:Type), Type.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Parameter mem: forall (a:Type), a -> (list a) -> Prop.
Implicit Arguments mem.
Axiom mem_def : forall (a:Type), forall (x:a) (l:(list a)),
match l with
| Nil => ~ (mem x l)
| Cons y r => (mem x l) <-> ((x = y) \/ (mem x r))
end.
Parameter infix_plpl: forall (a:Type), (list a) -> (list a) -> (list a).
Implicit Arguments infix_plpl.
Axiom infix_plpl_def : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
match l1 with
| Nil => ((infix_plpl l1 l2) = l2)
| Cons x1 r1 => ((infix_plpl l1 l2) = (Cons x1 (infix_plpl r1 l2)))
end.
Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
(Nil:(list a))) = l).
Parameter length: forall (a:Type), (list a) -> Z.
Implicit Arguments length.
Axiom length_def : forall (a:Type), forall (l:(list a)),
match l with
| Nil => ((length l) = 0%Z)
| Cons _ r => ((length l) = (1%Z + (length r))%Z)
end.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil:(list a))).
Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
(mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).
Inductive tree (a:Type) :=
| Leaf : a -> tree a
| Node : (tree a) -> (tree a) -> tree a.
Implicit Arguments Leaf.
Implicit Arguments Node.
Parameter labels: forall (a:Type), (tree a) -> (list a).
Implicit Arguments labels.
Axiom labels_def : forall (a:Type), forall (t:(tree a)),
match t with
| Leaf x => ((labels t) = (Cons x (Nil:(list a))))
| Node l r => ((labels t) = (infix_plpl (labels l) (labels r)))
end.
Axiom labels_Leaf : forall (a:Type), forall (x:a) (y:a), (mem x
(labels (Leaf y))) <-> (x = y).
Axiom labels_Node : forall (a:Type), forall (x:a) (l:(tree a)) (r:(tree a)),
(mem x (labels (Node l r))) <-> ((mem x (labels l)) \/ (mem x (labels r))).
Inductive same_shape{a:Type} {b:Type} : (tree a) -> (tree b) -> Prop :=
| same_shape_Leaf : forall (x1:a) (x2:b), (same_shape (Leaf x1) (Leaf x2))
| same_shape_Node : forall (l1:(tree a)) (r1:(tree a)) (l2:(tree b))
(r2:(tree b)), (same_shape l1 l2) -> ((same_shape r1 r2) ->
(same_shape (Node l1 r1) (Node l2 r2))).
Implicit Arguments same_shape.
Inductive distinct{a:Type} : (list a) -> Prop :=
| distinct_zero : (distinct (Nil:(list a)))
| distinct_one : forall (x:a), (distinct (Cons x (Nil:(list a))))
| distinct_many : forall (x:a) (l:(list a)), (~ (mem x l)) ->
((distinct l) -> (distinct (Cons x l))).
Implicit Arguments distinct.
Axiom distinct_append : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
(distinct l1) -> ((distinct l2) -> ((forall (x:a), (mem x l1) -> ~ (mem x
l2)) -> (distinct (infix_plpl l1 l2)))).
Parameter ref : forall (a:Type), Type.
Parameter r: Z.
Theorem WP_relabel : forall (a:Type), forall (t:(tree a)), forall (r1:Z),
match t with
| Leaf _ => True
| Node l r2 => forall (r3:Z), forall (result:(tree Z)), ((same_shape l
result) /\ ((distinct (labels result)) /\ ((r1 <= r3)%Z /\
forall (x:Z), (mem x (labels result)) -> ((r1 < x)%Z /\
(x <= r3)%Z)))) -> forall (r4:Z), forall (result1:(tree Z)),
((same_shape r2 result1) /\ ((distinct (labels result1)) /\
((r3 <= r4)%Z /\ forall (x:Z), (mem x (labels result1)) ->
((r3 < x)%Z /\ (x <= r4)%Z)))) -> ((same_shape t (Node result
result1)) /\ ((distinct (labels (Node result result1))) /\
((r1 <= r4)%Z /\ forall (x:Z), (mem x (labels (Node result
result1))) -> ((r1 < x)%Z /\ (x <= r4)%Z))))
end.
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
destruct t; intuition.
apply same_shape_Node; auto.
rewrite (labels_def _ (Node result result1)).
apply distinct_append; auto.
intro; red; intros.
assert (r1 < x <= r3)%Z.
apply H3; auto.
assert (r3 < x <= r4)%Z.
apply H7; auto.
omega.
rewrite (labels_def _ (Node result result1)) in H6.
generalize (mem_append _ x (labels result) (labels result1)); intuition.
generalize (H3 x); intuition.
generalize (H7 x); intuition.
rewrite (labels_def _ (Node result result1)) in H6.
generalize (mem_append _ x (labels result) (labels result1)); intuition.
generalize (H3 x); intuition.
generalize (H7 x); intuition.
Qed.
(* DO NOT EDIT BELOW *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment