From 24586c783ddcba4f0139fbf4cb47708090ba0e2a Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Tue, 18 Sep 2012 05:24:07 +0200 Subject: [PATCH] Playing with Coq realizations of polymorphic types --- lib/coq/list/Length.v | 37 +++++++++++++++++++++++++++++++++++++ lib/coq/list/List.v | 15 +++++++++++++++ 2 files changed, 52 insertions(+) create mode 100644 lib/coq/list/Length.v create mode 100644 lib/coq/list/List.v diff --git a/lib/coq/list/Length.v b/lib/coq/list/Length.v new file mode 100644 index 000000000..0e35c86c1 --- /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 000000000..26f55c8fa --- /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]]. + + -- GitLab