NthHdTl.v 1.55 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14 15 16 17 18 19 20
(* 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.Nth.
Require option.Option.
Require list.HdTl.
21

22
(* Why3 goal *)
23 24 25 26
Lemma Nth_tl {a:Type} {a_WT:WhyType a} :
  forall (l1:(list a)) (l2:(list a)),
  ((list.HdTl.tl l1) = (Init.Datatypes.Some l2)) -> forall (i:Z),
  ~ (i = (-1%Z)%Z) -> ((list.Nth.nth i l2) = (list.Nth.nth (i + 1%Z)%Z l1)).
27
Proof.
28
intros [|x1 l1] l2 h1 i h2.
29 30 31 32
easy.
simpl.
generalize (Zeq_bool_if (i + 1) 0).
case Zeq_bool.
33 34
intro H.
exfalso.
35 36 37 38 39 40 41 42 43
omega.
intros _.
simpl in h1.
inversion h1.
apply (f_equal (fun i => Nth.nth i l2)).
exact (Zpred_succ i).
Qed.

(* Why3 goal *)
44 45
Lemma Nth0_head {a:Type} {a_WT:WhyType a} :
  forall (l:(list a)), ((list.Nth.nth 0%Z l) = (list.HdTl.hd l)).
46
Proof.
47
now intros [|h t].
48 49
Qed.