Commit 91197648 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Restore Coq files that were inadvertently removed. (They contained the letter v.)

parent fb5858f6
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
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 x2: Z.
Parameter y2: Z.
Axiom first_octant : (0%Z <= (y2 ))%Z /\ ((y2 ) <= (x2 ))%Z.
Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
Definition best(x:Z) (y:Z): Prop := forall (yqt:Z),
((Zabs (((x2 ) * y)%Z - (x * (y2 ))%Z)%Z) <= (Zabs (((x2 ) * yqt)%Z - (x * (y2 ))%Z)%Z))%Z.
Definition invariant_(x:Z) (y:Z) (e:Z): Prop :=
(e = (((2%Z * (x + 1%Z)%Z)%Z * (y2 ))%Z - (((2%Z * y)%Z + 1%Z)%Z * (x2 ))%Z)%Z) /\
(((2%Z * ((y2 ) - (x2 ))%Z)%Z <= e)%Z /\ (e <= (2%Z * (y2 ))%Z)%Z).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(*s First a tactic [Case_Zabs] to do case split over [(Zabs x)]:
introduces two subgoals, one where [x] is assumed to be non negative
and thus where [Zabs x] is replaced by [x]; and another where
[x] is assumed to be non positive and thus where [Zabs x] is
replaced by [-x]. *)
Lemma Z_gt_le : forall x y:Z, (x > y)%Z -> (y <= x)%Z.
Proof.
intros; omega.
Qed.
Ltac Case_Zabs a Ha :=
elim (Z_le_gt_dec 0 a); intro Ha;
[ rewrite (Zabs_eq a Ha)
| rewrite (Zabs_non_eq a (Z_gt_le 0 a Ha)) ].
(*s A useful lemma to establish $|a| \le |b|$. *)
Lemma Zabs_le_Zabs :
forall a b:Z,
(b <= a <= 0)%Z \/ (0 <= a <= b)%Z -> (Zabs a <= Zabs b)%Z.
Proof.
intro a; Case_Zabs a Ha; intro b; Case_Zabs b Hb; omega.
Qed.
(*s A useful lemma to establish $|a| \le $. *)
Lemma Zabs_le :
forall a b:Z, (0 <= b)%Z -> ((Zopp b <= a <= b)%Z <-> (Zabs a <= b)%Z).
Proof.
intros a b Hb.
Case_Zabs a Ha; split; omega.
Qed.
(*s Two tactics. [ZCompare x y H] discriminates between [x<y], [x=y] and
[x>y] ([H] is the hypothesis name). [RingSimpl x y] rewrites [x] by [y]
using the [Ring] tactic. *)
Ltac ZCompare x y H :=
elim (Z_gt_le_dec x y); intro H;
[ idtac | elim (Z_le_lt_eq_dec x y H); clear H; intro H ].
Ltac RingSimpl x y := replace x with y; [ idtac | ring ].
(*s Key lemma for Bresenham's proof: if [b] is at distance less or equal
than [1/2] from the rational [c/a], then it is the closest such integer.
We express this property in [Z], thus multiplying everything by [2a]. *)
Lemma closest :
forall a b c:Z,
(0 <= a)%Z ->
(Zabs (2 * a * b - 2 * c) <= a)%Z ->
forall b':Z, (Zabs (a * b - c) <= Zabs (a * b' - c))%Z.
Proof.
intros a b c Ha Hmin.
generalize (proj2 (Zabs_le (2 * a * b - 2 * c) a Ha) Hmin).
intros Hmin' b'.
elim (Z_le_gt_dec (2 * a * b) (2 * c)); intro Habc.
(* 2ab <= 2c *)
rewrite (Zabs_non_eq (a * b - c)).
ZCompare b b' Hbb'.
(* b > b' *)
rewrite (Zabs_non_eq (a * b' - c)).
apply Zle_left_rev.
RingSimpl (Zopp (a * b' - c) + Zopp (Zopp (a * b - c)))%Z
(a * (b - b'))%Z.
apply Zmult_le_0_compat; omega.
apply Zge_le.
apply Zge_trans with (m := (a * b - c)%Z).
apply Zmult_ge_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
RingSimpl (a * b' - c)%Z (a * b' + Zopp c)%Z.
RingSimpl (a * b - c)%Z (a * b + Zopp c)%Z.
apply Zle_ge.
apply Zplus_le_compat_r.
apply Zmult_le_compat_l; omega.
(* b < b' *)
rewrite (Zabs_eq (a * b' - c)).
apply Zmult_le_reg_r with (p := 2%Z).
omega.
RingSimpl ((a * b' - c) * 2)%Z
(2 * (a * b' - a * b) + 2 * (a * b - c))%Z.
apply Zle_trans with a.
RingSimpl (Zopp (a * b - c) * 2)%Z (Zopp (2 * a * b - 2 * c)).
omega.
apply Zle_trans with (2 * a + Zopp a)%Z.
omega.
apply Zplus_le_compat.
RingSimpl (2 * a)%Z (2 * a * 1)%Z.
RingSimpl (2 * (a * b' - a * b))%Z (2 * a * (b' - b))%Z.
apply Zmult_le_compat_l; omega.
RingSimpl (2 * (a * b - c))%Z (2 * a * b - 2 * c)%Z.
omega.
(* 0 <= ab'-c *)
RingSimpl (a * b' - c)%Z (a * b' - a * b + (a * b - c))%Z.
RingSimpl 0%Z (a + Zopp a)%Z.
apply Zplus_le_compat.
RingSimpl a (a * 1)%Z.
RingSimpl (a * 1 * b' - a * 1 * b)%Z (a * (b' - b))%Z.
apply Zmult_le_compat_l; omega.
apply Zmult_le_reg_r with (p := 2%Z).
omega.
apply Zle_trans with (Zopp a).
omega.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
(* b = b' *)
rewrite <- Hbb'.
rewrite (Zabs_non_eq (a * b - c)).
omega.
apply Zge_le.
apply Zmult_ge_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
apply Zge_le.
apply Zmult_ge_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
(* 2ab > 2c *)
rewrite (Zabs_eq (a * b - c)).
ZCompare b b' Hbb'.
(* b > b' *)
rewrite (Zabs_non_eq (a * b' - c)).
apply Zmult_le_reg_r with (p := 2%Z).
omega.
RingSimpl (Zopp (a * b' - c) * 2)%Z
(2 * (c - a * b) + 2 * (a * b - a * b'))%Z.
apply Zle_trans with a.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
apply Zle_trans with (Zopp a + 2 * a)%Z.
omega.
apply Zplus_le_compat.
RingSimpl (2 * (c - a * b))%Z (2 * c - 2 * a * b)%Z.
omega.
RingSimpl (2 * a)%Z (2 * a * 1)%Z.
RingSimpl (2 * (a * b - a * b'))%Z (2 * a * (b - b'))%Z.
apply Zmult_le_compat_l; omega.
(* 0 >= ab'-c *)
RingSimpl (a * b' - c)%Z (a * b' - a * b + (a * b - c))%Z.
RingSimpl 0%Z (Zopp a + a)%Z.
apply Zplus_le_compat.
RingSimpl (Zopp a) (a * (-1))%Z.
RingSimpl (a * b' - a * b)%Z (a * (b' - b))%Z.
apply Zmult_le_compat_l; omega.
apply Zmult_le_reg_r with (p := 2%Z).
omega.
apply Zle_trans with a.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
omega.
(* b < b' *)
rewrite (Zabs_eq (a * b' - c)).
apply Zle_left_rev.
RingSimpl (a * b' - c + Zopp (a * b - c))%Z (a * (b' - b))%Z.
apply Zmult_le_0_compat; omega.
apply Zle_trans with (m := (a * b - c)%Z).
apply Zmult_le_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
RingSimpl (a * b' - c)%Z (a * b' + Zopp c)%Z.
RingSimpl (a * b - c)%Z (a * b + Zopp c)%Z.
apply Zplus_le_compat_r.
apply Zmult_le_compat_l; omega.
(* b = b' *)
rewrite <- Hbb'.
rewrite (Zabs_eq (a * b - c)).
omega.
apply Zmult_le_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
apply Zmult_le_reg_r with (p := 2%Z).
omega.
RingSimpl (0 * 2)%Z 0%Z.
RingSimpl ((a * b - c) * 2)%Z (2 * a * b - 2 * c)%Z.
omega.
Qed.
(* DO NOT EDIT BELOW *)
Theorem invariant_is_ok : forall (x:Z) (y:Z) (e:Z), (invariant_ x y e) ->
(best x y).
(* YOU MAY EDIT THE PROOF BELOW *)
Proof.
intros x y e.
unfold invariant_; unfold best; intros [E I'] y'.
cut (0 <= x2)%Z; [ intro Hx2 | idtac ].
apply closest.
assumption.
apply (proj1 (Zabs_le (2 * x2 * y - 2 * (x * y2)) x2 Hx2)).
rewrite E in I'.
split.
(* 0 <= x2 *)
generalize (proj2 I').
RingSimpl (2 * (x + 1) * y2 - (2 * y + 1) * x2)%Z
(2 * x * y2 - 2 * x2 * y + 2 * y2 - x2)%Z.
intro.
RingSimpl (2 * (x * y2))%Z (2 * x * y2)%Z.
omega.
(* 0 <= x2 *)
generalize (proj1 I').
RingSimpl (2 * (x + 1) * y2 - (2 * y + 1) * x2)%Z
(2 * x * y2 - 2 * x2 * y + 2 * y2 - x2)%Z.
RingSimpl (2 * (y2 - x2))%Z (2 * y2 - 2 * x2)%Z.
RingSimpl (2 * (x * y2))%Z (2 * x * y2)%Z.
omega.
omega.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import Zdiv.
Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
(x <= y)%Z).
Parameter sum_multiple_3_5_lt: Z -> Z.
Axiom SumEmpty : ((sum_multiple_3_5_lt 0%Z) = 0%Z).
Axiom SumNo : forall (n:Z), (0%Z <= n)%Z -> (((~ ((Zmod n 3%Z) = 0%Z)) /\
~ ((Zmod n 5%Z) = 0%Z)) ->
((sum_multiple_3_5_lt (n + 1%Z)%Z) = (sum_multiple_3_5_lt n))).
Axiom SumYes : forall (n:Z), (0%Z <= n)%Z -> ((((Zmod n 3%Z) = 0%Z) \/
((Zmod n 5%Z) = 0%Z)) ->
((sum_multiple_3_5_lt (n + 1%Z)%Z) = ((sum_multiple_3_5_lt n) + n)%Z)).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem div_minus1_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
(((Zmod (x + 1%Z)%Z y) = 0%Z) ->
((Zdiv (x + 1%Z)%Z y) = ((Zdiv x y) + 1%Z)%Z)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y (Hx,Hy) H.
pose (q := ((x+1)/ y)%Z).
assert (h2: (x = y * q - 1)%Z).
replace x with (x+1-1)%Z by omega.
rewrite (Z_div_mod_eq (x+1) y); auto with zarith.
rewrite H.
subst q; omega.
rewrite h2; clear h2.
replace (y * q - 1 + 1)%Z with (y*q)%Z by omega.
rewrite Zmult_comm.
rewrite Z_div_mult; auto with zarith.
replace (q*y-1)%Z with (q*y+(-1))%Z by omega.
rewrite Z_div_plus_full_l; auto with zarith.
assert (h:(y=1 \/ y > 1)%Z) by omega.
destruct h.
subst q y.
replace (-1 / 1)%Z with (-1)%Z.
omega.
rewrite Zdiv_1_r; auto.
replace (-1)%Z with (-(1))%Z; auto with zarith.
rewrite (Z_div_nz_opp_full 1 y).
rewrite Zdiv_1_l; auto with zarith.
rewrite Zmod_1_l; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
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.
Parameter ref : forall (a:Type), Type.
Parameter t : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (t a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (t a b) -> a -> b -> (t a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(t a b)), forall (a1:a)
(a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(t a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter create_const: forall (b:Type) (a:Type), b -> (t a b).
Set Contextual Implicit.
Implicit Arguments create_const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
((get (create_const(b1):(t a b)) a1) = b1).
Parameter pointer : Type.
Definition next := (t pointer pointer).
Parameter null: pointer.
Parameter value: (t pointer Z).
Parameter next1: (t pointer pointer).
Inductive is_list : (t pointer pointer) -> pointer -> Prop :=
| is_list_null : forall (next2:(t pointer pointer)) (p:pointer),
(p = (null )) -> (is_list next2 p)
| is_list_next : forall (next3:(t pointer pointer)) (p:pointer),
(~ (p = (null ))) -> ((is_list next3 (get next3 p)) -> (is_list next3
p)).
Parameter ft : forall (a:Type), Type.
Parameter in_ft: pointer -> (ft pointer) -> Prop.
Parameter list_ft: (t pointer pointer) -> pointer -> (ft pointer).
Axiom list_ft_node_null_cor : forall (next4:(t pointer pointer)) (q:pointer)
(p:pointer), (q = (null )) -> ~ (in_ft p (list_ft next4 q)).
Axiom list_ft_node_next1 : forall (next5:(t pointer pointer)) (q:pointer)
(p:pointer), (~ (q = (null ))) -> ((is_list next5 (get next5 q)) ->
((in_ft p (list_ft next5 (get next5 q))) -> (in_ft p (list_ft next5 q)))).
Axiom list_ft_node_next2 : forall (next6:(t pointer pointer)) (q:pointer),
(~ (q = (null ))) -> ((is_list next6 (get next6 q)) -> (in_ft q
(list_ft next6 q))).
Axiom list_ft_node_next_inv : forall (next7:(t pointer pointer)) (q:pointer)
(p:pointer), (~ (q = (null ))) -> ((is_list next7 (get next7 q)) ->
((~ (q = p)) -> ((in_ft p (list_ft next7 q)) -> (in_ft p (list_ft next7
(get next7 q)))))).
Theorem frame_list : forall (next8:(t pointer pointer)) (p:pointer)
(q:pointer) (v:pointer), (~ (in_ft q (list_ft next8 p))) -> ((is_list next8
p) -> (is_list (set next8 q v) p)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
induction H0.
apply (is_list_null _ _ H0).
apply (is_list_next _ _ H0).
assert (q<>p) by (intro eq;apply H;rewrite eq;clear eq;apply (list_ft_node_next2 _ _ H0 H1)).
rewrite (Select_neq _ _ _ _ _ _ H2).
apply IHis_list.
contradict H.
exact (list_ft_node_next1 _ _ _ H0 H1 H).
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
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 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.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
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).
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)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Parameter pointer : Type.
Axiom pointer_dec : forall (p1:pointer) (p2:pointer), (p1 = p2) \/
~ (p1 = p2).
Definition next := (map pointer pointer).
Parameter null: pointer.
Parameter value: (ref (map pointer Z)).
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)).
Parameter ft : forall (a:Type), Type.
Parameter in_ft: pointer -> (ft pointer) -> Prop.
Axiom set_eq : forall (ft1:(ft pointer)) (ft2:(ft pointer)),
(forall (q:pointer), (in_ft q ft1) <-> (in_ft q ft2)) -> (ft1 = ft2).
Parameter list_ft: (map pointer pointer) -> pointer -> (ft pointer).
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)))).
Axiom list_ft_node_next2 : forall (next2:(map pointer pointer)) (q:pointer),
(~ (q = (null ))) -> ((is_list next2 (get 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)))))).
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)).
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))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
apply set_eq.
intros.
split;intro.
(** First part *)
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))
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).
rewrite <- H4.
exact (list_ft_node_next2 _ p H0 H2').
(* p <> q0 *)
apply (list_ft_node_next1 _ _ _ H0 H2').
rewrite (Select_neq _ _ _ _ _ _ H3).
apply IHis_list.
contradict H;exact (list_ft_node_next1 _ _ _ H0 H2 H).
exact (list_ft_node_next_inv _ _ _ H0 H2 H4 H1).
(** Second part *)
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))
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).
rewrite <- H4.
exact (list_ft_node_next2 _ p H0 H2).
(* p <> q0 *)
apply (list_ft_node_next1 _ _ _ H0 H2).
apply IHis_list.
contradict H;exact (list_ft_node_next1 _ _ _ H0 H2 H).
rewrite <- (Select_neq _ _ _ _ _ v H3).
exact (list_ft_node_next_inv _ _ _ H0 H2' H4 H1).
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter label : Type.