diff --git a/lib/coq/list/Length.v b/lib/coq/list/Length.v new file mode 100644 index 0000000000000000000000000000000000000000..0e35c86c159e0ff426b6a1b5809235b8407b5648 --- /dev/null +++ b/lib/coq/list/Length.v @@ -0,0 +1,37 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require int.Int. + +(* Why3 assumption *) +Inductive list (a:Type) {a_WT:WhyType a} := + | Nil : list a + | Cons : a -> (list a) -> list a. +Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). +Existing Instance list_WhyType. +Implicit Arguments Nil [[a] [a_WT]]. +Implicit Arguments Cons [[a] [a_WT]]. + +(* Why3 assumption *) +Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z := + match l with + | Nil => 0%Z + | (Cons _ r) => (1%Z + (length r))%Z + end. + +(* Why3 goal *) +Lemma Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list + a)), (0%Z <= (length l))%Z. +intros a a_WT l. + +Qed. + +(* Why3 goal *) +Lemma Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + ((length l) = 0%Z) <-> (l = (Nil :(list a))). +intros a a_WT l. + +Qed. + + diff --git a/lib/coq/list/List.v b/lib/coq/list/List.v new file mode 100644 index 0000000000000000000000000000000000000000..26f55c8fac2289a1ae7a0398a9f14da58bfdda69 --- /dev/null +++ b/lib/coq/list/List.v @@ -0,0 +1,15 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. + +(* Why3 assumption *) +Inductive list (a:Type) {a_WT:WhyType a} := + | Nil : list a + | Cons : a -> (list a) -> list a. +Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). +Existing Instance list_WhyType. +Implicit Arguments Nil [[a] [a_WT]]. +Implicit Arguments Cons [[a] [a_WT]]. + +