Commit 59bc2ab0 authored by MARCHE Claude's avatar MARCHE Claude

update proof

parent aee9523c
......@@ -6,11 +6,11 @@ Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
......@@ -44,7 +44,7 @@ Implicit Arguments None.
Unset Contextual Implicit.
Implicit Arguments Some.
Parameter nth: forall (a:Type), Z -> (list a) -> (option a).
Parameter nth: forall (a:Type), Z -> (list a) -> (option a).
Implicit Arguments nth.
......@@ -85,18 +85,11 @@ Definition tl (a:Type)(l:(list a)): (option (list a)) :=
end.
Implicit Arguments tl.
Theorem WP_parameter_search_loop : forall (l:(list Z)), forall (s:(list Z)),
forall (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 (result:Z),
(match s with
| Nil => (None:(option Z))
| Cons h _ => (Some h)
end = (Some result)) -> ((result = 0%Z) -> ((((0%Z <= i)%Z /\
(i < (length l))%Z) /\ (zero_at l i)) \/ ((i = (length l)) /\
(no_zero l)))))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_search_loop : True.
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
destruct s.
......
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