updated Coq proof

parent 8c721d48
......@@ -18,34 +18,43 @@ Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition ref (a:Type) := a.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Parameter mixfix_lbrb: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Implicit Arguments mixfix_lbrb.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Parameter mixfix_lblsmnrb: forall (a:Type) (b:Type), (map a b) -> a -> b ->
(map a b).
Implicit Arguments set.
Implicit Arguments mixfix_lblsmnrb.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((mixfix_lbrb (mixfix_lblsmnrb m a1 b1) a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) ->
((mixfix_lbrb (mixfix_lblsmnrb m a1 b1) a2) = (mixfix_lbrb m a2)).
Parameter create_const: forall (b:Type) (a:Type), b -> (map a b).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments create_const.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
((get (create_const(b1):(map a b)) a1) = b1).
((mixfix_lbrb (const(b1):(map a b)) a1) = b1).
Parameter pointer : Type.
......@@ -57,18 +66,18 @@ Definition next := (map pointer pointer).
Parameter null: pointer.
Parameter value: (map pointer Z).
Parameter value: (ref (map pointer Z)).
Parameter next1: (map pointer pointer).
Parameter next1: (ref (map pointer pointer)).
Inductive is_list : (map pointer pointer) -> pointer -> Prop :=
| is_list_null : forall (next2:(map pointer pointer)) (p:pointer),
(p = (null )) -> (is_list next2 p)
| is_list_next : forall (next2:(map pointer pointer)) (p:pointer),
(~ (p = (null ))) -> ((is_list next2 (get next2 p)) -> (is_list next2
p)).
(~ (p = (null ))) -> ((is_list next2 (mixfix_lbrb next2 p)) ->
(is_list next2 p)).
Parameter ft : forall (a:Type), Type.
......@@ -85,28 +94,29 @@ Axiom list_ft_node_null_cor : forall (next2:(map pointer pointer))
(q:pointer) (p:pointer), (q = (null )) -> ~ (in_ft p (list_ft next2 q)).
Axiom list_ft_node_next1 : forall (next2:(map pointer pointer)) (q:pointer)
(p:pointer), (~ (q = (null ))) -> ((is_list next2 (get next2 q)) ->
((in_ft p (list_ft next2 (get next2 q))) -> (in_ft p (list_ft next2 q)))).
(p:pointer), (~ (q = (null ))) -> ((is_list next2 (mixfix_lbrb next2 q)) ->
((in_ft p (list_ft next2 (mixfix_lbrb next2 q))) -> (in_ft p (list_ft next2
q)))).
Axiom list_ft_node_next2 : forall (next2:(map pointer pointer)) (q:pointer),
(~ (q = (null ))) -> ((is_list next2 (get next2 q)) -> (in_ft q
(~ (q = (null ))) -> ((is_list next2 (mixfix_lbrb next2 q)) -> (in_ft q
(list_ft next2 q))).
Axiom list_ft_node_next_inv : forall (next2:(map pointer pointer))
(q:pointer) (p:pointer), (~ (q = (null ))) -> ((is_list next2 (get next2
q)) -> ((~ (q = p)) -> ((in_ft p (list_ft next2 q)) -> (in_ft p
(list_ft next2 (get next2 q)))))).
(q:pointer) (p:pointer), (~ (q = (null ))) -> ((is_list next2
(mixfix_lbrb next2 q)) -> ((~ (q = p)) -> ((in_ft p (list_ft next2 q)) ->
(in_ft p (list_ft next2 (mixfix_lbrb next2 q)))))).
Axiom frame_list : forall (next2:(map pointer pointer)) (p:pointer)
(q:pointer) (v:pointer), (~ (in_ft q (list_ft next2 p))) -> ((is_list next2
p) -> (is_list (set next2 q v) p)).
p) -> (is_list (mixfix_lblsmnrb next2 q v) p)).
Definition sep_node_list(next2:(map pointer pointer)) (p1:pointer)
(p2:pointer): Prop := ~ (in_ft p1 (list_ft next2 p2)).
Theorem frame_list_ft : forall (next2:(map pointer pointer)) (p:pointer)
(q:pointer) (v:pointer), (~ (in_ft q (list_ft next2 p))) -> ((is_list next2
p) -> ((list_ft next2 p) = (list_ft (set next2 q v) p))).
p) -> ((list_ft next2 p) = (list_ft (mixfix_lblsmnrb next2 q v) p))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
apply set_eq.
......@@ -117,7 +127,7 @@ induction H0.
apply (list_ft_node_null_cor _ _ _ H0) in H1;contradiction.
(* some asserts *)
assert (q<>p) by (intro eq;apply H;rewrite eq;clear eq;apply (list_ft_node_next2 _ _ H0 H2)).
assert (H2' : is_list (set next2 q v) (get (set next2 q v) p))
assert (H2' : is_list (mixfix_lblsmnrb next2 q v) (mixfix_lbrb (mixfix_lblsmnrb next2 q v) p))
by (rewrite (Select_neq _ _ _ _ _ v H3);refine (frame_list _ _ _ _ _ H2);contradict H;exact (list_ft_node_next1 _ _ _ H0 H2 H)).
(* *)
destruct (pointer_dec p q0).
......@@ -134,7 +144,7 @@ induction H0.
apply (list_ft_node_null_cor _ _ _ H0) in H1;contradiction.
(* some asserts *)
assert (q<>p) by (intro eq;apply H;rewrite eq;clear eq;apply (list_ft_node_next2 _ _ H0 H2)).
assert (H2' : is_list (set next2 q v) (get (set next2 q v) p))
assert (H2' : is_list (mixfix_lblsmnrb next2 q v) (mixfix_lbrb (mixfix_lblsmnrb next2 q v) p))
by (rewrite (Select_neq _ _ _ _ _ v H3);refine (frame_list _ _ _ _ _ H2);contradict H;exact (list_ft_node_next1 _ _ _ H0 H2 H)).
(* *)
destruct (pointer_dec p q0).
......
......@@ -28,9 +28,9 @@
<result status="valid" time="0.50"/>
</proof>
</goal>
<goal name="frame_list_ft" sum="d0c0dd407e6667c967cd37f14169af5e" proved="false" expanded="true">
<goal name="frame_list_ft" sum="d0c0dd407e6667c967cd37f14169af5e" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_list_ft_1.v" obsolete="false">
<result status="unknown" time="0.48"/>
<result status="valid" time="0.54"/>
</proof>
</goal>
<goal name="acyclic_list" sum="9beb2427d92c0d05c7ab34738d84fb20" proved="false" expanded="true">
......
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