NthLength.v 1.43 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Nth.
Require option.Option.

(* Why3 goal *)
Lemma nth_none_1 : forall {a:Type} {a_WT:WhyType a}, forall (l:list a) (i:Z),
  (i < 0%Z)%Z -> ((list.Nth.nth i l) = None).
Proof.
intros a a_WT l.
induction l as [|h q].
easy.
intros i H.
simpl.
generalize (Zeq_bool_if i 0).
case Zeq_bool.
intros H'.
now rewrite H' in H.
intros _.
apply IHq.
omega.
Qed.

(* Why3 goal *)
Lemma nth_none_2 : forall {a:Type} {a_WT:WhyType a}, forall (l:list a) (i:Z),
  ((list.Length.length l) <= i)%Z -> ((list.Nth.nth i l) = None).
Proof.
intros a a_WT l.
induction l as [|h q].
easy.
intros i H.
unfold Length.length in H.
fold Length.length in H.
simpl.
generalize (Zeq_bool_if i 0).
case Zeq_bool.
intros H'.
rewrite H' in H.
generalize (Length.Length_nonnegative q).
omega.
intros _.
apply IHq.
omega.
Qed.

(* Why3 goal *)
Lemma nth_none_3 : forall {a:Type} {a_WT:WhyType a}, forall (l:list a) (i:Z),
  ((list.Nth.nth i l) = None) -> ((i < 0%Z)%Z \/
  ((list.Length.length l) <= i)%Z).
Proof.
intros a a_WT l.
induction l as [|h q].
intros i _.
simpl.
omega.
intros i.
simpl (Nth.nth i (h :: q)).
change (Length.length (h :: q)) with (1 + Length.length q)%Z.
generalize (Zeq_bool_if i 0).
case Zeq_bool.
easy.
intros Hi H.
specialize (IHq _ H).
omega.
Qed.