Commit c2b382a7 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix Coq proofs for examples/vstte10_search_list.mlw.

parent e8058a50
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Nth.
Require option.Option.
Require list.HdTl.
(* Why3 assumption *)
Definition unit := unit.
Definition unit := unit.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
Definition zero_at (l:(list Z)) (i:Z): Prop := ((list.Nth.nth i
l) = (Some 0%Z)) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) ->
~ ((list.Nth.nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Fixpoint length {a:Type}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (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))).
(* Why3 assumption *)
Inductive option (a:Type) :=
| None : option a
| Some : a -> option a.
Implicit Arguments None [[a]].
Implicit Arguments Some [[a]].
Parameter nth: forall {a:Type}, Z -> (list a) -> (option a).
Axiom nth_def : forall {a:Type}, forall (n:Z) (l:(list a)),
match l with
| Nil => ((nth n l) = (None :(option a)))
| (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
((nth n l) = (nth (n - 1%Z)%Z r)))
end.
(* Why3 assumption *)
Definition zero_at(l:(list Z)) (i:Z): Prop := ((nth i l) = (Some 0%Z)) /\
forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Definition no_zero(l:(list Z)): Prop := forall (j:Z), ((0%Z <= j)%Z /\
(j < (length l))%Z) -> ~ ((nth j l) = (Some 0%Z)).
Definition no_zero (l:(list Z)): Prop := forall (j:Z), ((0%Z <= j)%Z /\
(j < (list.Length.length l))%Z) -> ~ ((list.Nth.nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Inductive ref (a:Type) :=
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref [[a]].
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type}(v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Definition hd {a:Type}(l:(list a)): (option a) :=
match l with
| Nil => (None :(option a))
| (Cons h _) => (Some h)
end.
(* Why3 assumption *)
Definition tl {a:Type}(l:(list a)): (option (list a)) :=
match l with
| Nil => (None :(option (list a)))
| (Cons _ t) => (Some t)
end.
(* Why3 goal *)
Theorem WP_parameter_search_loop : forall (l:(list Z)), forall (s:(list Z))
(i:Z), ((0%Z <= i)%Z /\ (((i + (length s))%Z = (length l)) /\
((forall (j:Z), (0%Z <= j)%Z -> ((nth j s) = (nth (i + j)%Z l))) /\
forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j
l) = (Some 0%Z))))) -> ((~ (s = (Nil :(list Z)))) -> ((~ (s = (Nil :(list
Z)))) -> forall (o:Z),
(i:Z), ((0%Z <= i)%Z /\
(((i + (list.Length.length s))%Z = (list.Length.length l)) /\
((forall (j:Z), (0%Z <= j)%Z -> ((list.Nth.nth j
s) = (list.Nth.nth (i + j)%Z l))) /\ forall (j:Z), ((0%Z <= j)%Z /\
(j < i)%Z) -> ~ ((list.Nth.nth j l) = (Some 0%Z))))) -> ((~ (s = nil)) ->
((~ (s = nil)) -> forall (o:Z),
match s with
| Nil => False
| (Cons h _) => (o = h)
end -> ((o = 0%Z) -> ((((0%Z <= i)%Z /\ (i < (length l))%Z) /\ (zero_at l
i)) \/ ((i = (length l)) /\ (no_zero l)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
| nil => False
| (cons h _) => (o = h)
end -> ((o = 0%Z) -> ((((0%Z <= i)%Z /\ (i < (list.Length.length l))%Z) /\
(zero_at l i)) \/ ((i = (list.Length.length l)) /\ (no_zero l)))))).
(* Why3 intros l s i (h1,(h2,(h3,h4))) h5 h6 o h7 h8. *)
intuition.
destruct s.
destruct H4.
......@@ -97,17 +56,15 @@ subst; subst.
clear H0 H1.
left.
split.
replace (length (Cons 0 s))%Z with (1 + length s)%Z in H by auto.
generalize (Length_nonnegative s).
change (Length.length (cons 0 s))%Z with (1 + Length.length s)%Z in H.
generalize (Length.Length_nonnegative s).
omega.
red; intuition.
assert (H0: (0 <= 0)%Z) by omega.
generalize (H3 0%Z H0).
generalize (nth_def 0%Z (Cons 0%Z s)).
generalize (Nth.nth_def 0%Z (cons 0%Z s)).
ring_simplify (i+0)%Z.
intuition.
rewrite H4 in H1.
auto.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Nth.
Require option.Option.
Require list.HdTl.
(* Why3 assumption *)
Definition unit := unit.
Definition unit := unit.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
Definition zero_at (l:(list Z)) (i:Z): Prop := ((list.Nth.nth i
l) = (Some 0%Z)) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) ->
~ ((list.Nth.nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Fixpoint length {a:Type}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (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))).
(* Why3 assumption *)
Inductive option (a:Type) :=
| None : option a
| Some : a -> option a.
Implicit Arguments None [[a]].
Implicit Arguments Some [[a]].
Parameter nth: forall {a:Type}, Z -> (list a) -> (option a).
Axiom nth_def : forall {a:Type}, forall (n:Z) (l:(list a)),
match l with
| Nil => ((nth n l) = (None :(option a)))
| (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
((nth n l) = (nth (n - 1%Z)%Z r)))
end.
(* Why3 assumption *)
Definition zero_at(l:(list Z)) (i:Z): Prop := ((nth i l) = (Some 0%Z)) /\
forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Definition no_zero(l:(list Z)): Prop := forall (j:Z), ((0%Z <= j)%Z /\
(j < (length l))%Z) -> ~ ((nth j l) = (Some 0%Z)).
Definition no_zero (l:(list Z)): Prop := forall (j:Z), ((0%Z <= j)%Z /\
(j < (list.Length.length l))%Z) -> ~ ((list.Nth.nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Inductive ref (a:Type) :=
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref [[a]].
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type}(v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Definition hd {a:Type}(l:(list a)): (option a) :=
match l with
| Nil => (None :(option a))
| (Cons h _) => (Some h)
end.
(* Why3 assumption *)
Definition tl {a:Type}(l:(list a)): (option (list a)) :=
match l with
| Nil => (None :(option (list a)))
| (Cons _ t) => (Some t)
end.
(* Why3 goal *)
Theorem WP_parameter_search_loop : forall (l:(list Z)), forall (s:(list Z))
(i:Z), ((0%Z <= i)%Z /\ (((i + (length s))%Z = (length l)) /\
((forall (j:Z), (0%Z <= j)%Z -> ((nth j s) = (nth (i + j)%Z l))) /\
forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j
l) = (Some 0%Z))))) -> ((~ (s = (Nil :(list Z)))) -> ((~ (s = (Nil :(list
Z)))) -> forall (o:Z),
(i:Z), ((0%Z <= i)%Z /\
(((i + (list.Length.length s))%Z = (list.Length.length l)) /\
((forall (j:Z), (0%Z <= j)%Z -> ((list.Nth.nth j
s) = (list.Nth.nth (i + j)%Z l))) /\ forall (j:Z), ((0%Z <= j)%Z /\
(j < i)%Z) -> ~ ((list.Nth.nth j l) = (Some 0%Z))))) -> ((~ (s = nil)) ->
((~ (s = nil)) -> forall (o:Z),
match s with
| Nil => False
| (Cons h _) => (o = h)
| nil => False
| (cons h _) => (o = h)
end -> ((~ (o = 0%Z)) -> forall (i1:Z), (i1 = (i + 1%Z)%Z) ->
((~ (s = (Nil :(list Z)))) -> forall (o1:(list Z)),
((~ (s = nil)) -> forall (o1:(list Z)),
match s with
| Nil => False
| (Cons _ t) => (o1 = t)
| nil => False
| (cons _ t) => (o1 = t)
end -> forall (s1:(list Z)), (s1 = o1) -> forall (j:Z), (0%Z <= j)%Z ->
((nth j s1) = (nth (i1 + j)%Z l)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
((list.Nth.nth j s1) = (list.Nth.nth (i1 + j)%Z l)))))).
(* Why3 intros l s i (h1,(h2,(h3,h4))) h5 h6 o h7 h8 i1 h9 h10 o1 h11 s1 h12
j h13. *)
intuition.
destruct s.
destruct H9.
subst.
assert (hj: (0 <= j+1)%Z) by omega.
generalize (H3 (j+1)%Z hj).
generalize (nth_def (j+1)%Z (Cons z s)).
generalize (Nth.nth_def (j+1)%Z (cons z s)).
intuition.
ring_simplify (j+1-1)%Z in H4.
ring_simplify (i+(j+1))%Z in H7.
ring_simplify (i+1+j)%Z.
transitivity (nth (j + 1) (Cons z s)); auto.
transitivity (Nth.nth (j + 1) (cons z s)); auto.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Nth.
Require option.Option.
Require list.HdTl.
(* Why3 assumption *)
Definition unit := unit.
Definition unit := unit.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
Definition zero_at (l:(list Z)) (i:Z): Prop := ((list.Nth.nth i
l) = (Some 0%Z)) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) ->
~ ((list.Nth.nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Fixpoint length {a:Type}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (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))).
(* Why3 assumption *)
Inductive option (a:Type) :=
| None : option a
| Some : a -> option a.
Implicit Arguments None [[a]].
Implicit Arguments Some [[a]].
Parameter nth: forall {a:Type}, Z -> (list a) -> (option a).
Axiom nth_def : forall {a:Type}, forall (n:Z) (l:(list a)),
match l with
| Nil => ((nth n l) = (None :(option a)))
| (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
((nth n l) = (nth (n - 1%Z)%Z r)))
end.
(* Why3 assumption *)
Definition zero_at(l:(list Z)) (i:Z): Prop := ((nth i l) = (Some 0%Z)) /\
forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Definition no_zero(l:(list Z)): Prop := forall (j:Z), ((0%Z <= j)%Z /\
(j < (length l))%Z) -> ~ ((nth j l) = (Some 0%Z)).
Definition no_zero (l:(list Z)): Prop := forall (j:Z), ((0%Z <= j)%Z /\
(j < (list.Length.length l))%Z) -> ~ ((list.Nth.nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Inductive ref (a:Type) :=
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref [[a]].
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type}(v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Definition hd {a:Type}(l:(list a)): (option a) :=
match l with
| Nil => (None :(option a))
| (Cons h _) => (Some h)
end.
(* Why3 assumption *)
Definition tl {a:Type}(l:(list a)): (option (list a)) :=
match l with
| Nil => (None :(option (list a)))
| (Cons _ t) => (Some t)
end.
(* Why3 goal *)
Theorem WP_parameter_search_loop : forall (l:(list Z)), forall (s:(list Z))
(i:Z), ((0%Z <= i)%Z /\ (((i + (length s))%Z = (length l)) /\
((forall (j:Z), (0%Z <= j)%Z -> ((nth j s) = (nth (i + j)%Z l))) /\
forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j
l) = (Some 0%Z))))) -> ((~ (s = (Nil :(list Z)))) -> ((~ (s = (Nil :(list
Z)))) -> forall (o:Z),
(i:Z), ((0%Z <= i)%Z /\
(((i + (list.Length.length s))%Z = (list.Length.length l)) /\
((forall (j:Z), (0%Z <= j)%Z -> ((list.Nth.nth j
s) = (list.Nth.nth (i + j)%Z l))) /\ forall (j:Z), ((0%Z <= j)%Z /\
(j < i)%Z) -> ~ ((list.Nth.nth j l) = (Some 0%Z))))) -> ((~ (s = nil)) ->
((~ (s = nil)) -> forall (o:Z),
match s with
| Nil => False
| (Cons h _) => (o = h)
| nil => False
| (cons h _) => (o = h)
end -> ((~ (o = 0%Z)) -> forall (i1:Z), (i1 = (i + 1%Z)%Z) ->
((~ (s = (Nil :(list Z)))) -> forall (o1:(list Z)),
((~ (s = nil)) -> forall (o1:(list Z)),
match s with
| Nil => False
| (Cons _ t) => (o1 = t)
| nil => False
| (cons _ t) => (o1 = t)
end -> forall (s1:(list Z)), (s1 = o1) -> forall (j:Z), ((0%Z <= j)%Z /\
(j < i1)%Z) -> ~ ((nth j l) = (Some 0%Z)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
(j < i1)%Z) -> ~ ((list.Nth.nth j l) = (Some 0%Z)))))).
(* Why3 intros l s i (h1,(h2,(h3,h4))) h5 h6 o h7 h8 i1 h9 h10 o1 h11 s1 h12
j (h13,h14). *)
intuition.
destruct s.
destruct H9.
subst.
replace (length (Cons z s)) with (1 + length s)%Z in H by auto.
change (Length.length (cons z s)) with (1 + Length.length s)%Z in H.
assert (h: (j < i \/ j= i)%Z) by omega; destruct h.
apply (H5 j); auto with *.
subst j.
......@@ -106,7 +66,7 @@ apply H6.
clear H0 H1 H8.
assert (H0: (0 <= 0)%Z) by omega.
generalize (H3 0%Z H0).
generalize (nth_def 0%Z (Cons z s)).
generalize (Nth.nth_def 0%Z (cons z s)).
intuition.
ring_simplify (i+0)%Z in H4.
clear H8.
......
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