From 6b0c7b82741650be7b425735eb40326c84e0c5b1 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 12 Jun 2013 15:58:46 +0200 Subject: [PATCH] Realize some more theories about lists. Fix an inconsistent axiom along the way. --- Makefile.in | 2 +- drivers/coq-common.gen | 10 ++++- lib/coq/list/Append.v | 85 ++++++++++++++++++++++++++++++++++++++++ lib/coq/list/HdTl.v | 22 +++++++++++ lib/coq/list/Length.v | 24 ++++++++---- lib/coq/list/Mem.v | 30 ++++++++++++++ lib/coq/list/Nth.v | 5 ++- lib/coq/list/NthHdTl.v | 37 +++++++++++++++++ lib/coq/list/NthLength.v | 12 +++--- theories/list.why | 2 +- 10 files changed, 209 insertions(+), 20 deletions(-) create mode 100644 lib/coq/list/Append.v create mode 100644 lib/coq/list/HdTl.v create mode 100644 lib/coq/list/Mem.v create mode 100644 lib/coq/list/NthHdTl.v diff --git a/Makefile.in b/Makefile.in index 186c85260..f0e4a6e97 100644 --- a/Makefile.in +++ b/Makefile.in @@ -828,7 +828,7 @@ COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES)) COQLIBS_MAP_FILES = Map MapPermut COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES)) -COQLIBS_LIST_FILES = List Length Nth NthLength +COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES)) COQLIBS_OPTION_FILES = Option diff --git a/drivers/coq-common.gen b/drivers/coq-common.gen index 08aae20c2..594744a92 100644 --- a/drivers/coq-common.gen +++ b/drivers/coq-common.gen @@ -273,15 +273,21 @@ end theory list.List - syntax type list "list %1" + syntax type list "(list %1)" syntax function Nil "nil" syntax function Cons "(cons %1 %2)" end +theory list.Append + + syntax function (++) "(List.app %1 %2)" + +end + theory option.Option - syntax type option "option %1" + syntax type option "(option %1)" syntax function None "None" syntax function Some "(Some %1)" diff --git a/lib/coq/list/Append.v b/lib/coq/list/Append.v new file mode 100644 index 000000000..21a302f51 --- /dev/null +++ b/lib/coq/list/Append.v @@ -0,0 +1,85 @@ +(* 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.Mem. + +(* Why3 goal *) +Lemma infix_plpl_def {a:Type} {a_WT:WhyType a}: forall (l1:(list a)) + (l2:(list a)), + ((List.app l1 l2) = match l1 with + | nil => l2 + | (cons x1 r1) => (cons x1 (List.app r1 l2)) + end). +Proof. +now intros [|h1 q1] l2. +Qed. + +Require Import Lists.List. + +(* Why3 goal *) +Lemma Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (l3:(list a)), + ((List.app l1 (List.app l2 l3)) = (List.app (List.app l1 l2) l3)). +Proof. +intros a a_WT l1 l2 l3. +apply app_assoc. +Qed. + +(* Why3 goal *) +Lemma Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + ((List.app l nil) = l). +Proof. +intros a a_WT l. +apply app_nil_r. +Qed. + +(* Why3 goal *) +Lemma Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)), + ((list.Length.length (List.app l1 l2)) = ((list.Length.length l1) + (list.Length.length l2))%Z). +Proof. +intros a a_WT l1 l2. +rewrite 3!Length.length_std. +now rewrite app_length, inj_plus. +Qed. + +(* Why3 goal *) +Lemma mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) + (l1:(list a)) (l2:(list a)), (list.Mem.mem x (List.app l1 l2)) <-> + ((list.Mem.mem x l1) \/ (list.Mem.mem x l2)). +Proof. +intros a a_WT x l1 l2. +split. +intros H. +apply Mem.mem_std in H. +apply in_app_or in H. +destruct H as [H|H]. +left. +now apply Mem.mem_std. +right. +now apply Mem.mem_std. +intros H. +apply Mem.mem_std. +apply in_or_app. +destruct H as [H|H]. +left. +now apply Mem.mem_std. +right. +now apply Mem.mem_std. +Qed. + +(* Why3 goal *) +Lemma mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) + (l:(list a)), (list.Mem.mem x l) -> exists l1:(list a), exists l2:(list a), + (l = (List.app l1 (cons x l2))). +Proof. +intros a a_WT x l h1. +apply in_split. +now apply Mem.mem_std. +Qed. + + diff --git a/lib/coq/list/HdTl.v b/lib/coq/list/HdTl.v new file mode 100644 index 000000000..0f942dda8 --- /dev/null +++ b/lib/coq/list/HdTl.v @@ -0,0 +1,22 @@ +(* This file is generated by Why3's Coq-realize driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require list.List. +Require option.Option. + +(* Why3 assumption *) +Definition hd {a:Type} {a_WT:WhyType a} (l:(list a)): (option a) := + match l with + | nil => None + | (cons h _) => (Some h) + end. + +(* Why3 assumption *) +Definition tl {a:Type} {a_WT:WhyType a} (l:(list a)): (option (list a)) := + match l with + | nil => None + | (cons _ t) => (Some t) + end. + + diff --git a/lib/coq/list/Length.v b/lib/coq/list/Length.v index 4f03911e3..1a45cea59 100644 --- a/lib/coq/list/Length.v +++ b/lib/coq/list/Length.v @@ -6,26 +6,34 @@ Require int.Int. Require list.List. (* Why3 assumption *) -Fixpoint length {a:Type} {a_WT:WhyType a} (l:list a) {struct l}: Z := +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. +Lemma length_std : + forall {a:Type} {a_WT:WhyType a} (l:list a), + length l = Z_of_nat (List.length l). +Proof. +intros a a_WT l. +induction l. +easy. +change (1 + length l = Z.of_nat (S (List.length l)))%Z. +now rewrite inj_S, Zplus_comm, IHl. +Qed. + (* Why3 goal *) Lemma Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, - forall (l:list a), (0%Z <= (length l))%Z. + forall (l:(list a)), (0%Z <= (length l))%Z. Proof. intros a a_WT l. -induction l as [|h t]. -apply Zle_refl. -unfold length. -fold length. -omega. +rewrite length_std. +apply Zle_0_nat. Qed. (* Why3 goal *) -Lemma Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:list a), +Lemma Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((length l) = 0%Z) <-> (l = nil). Proof. intros a a_WT [|h t] ; split ; try easy. diff --git a/lib/coq/list/Mem.v b/lib/coq/list/Mem.v new file mode 100644 index 000000000..03f4d0fa3 --- /dev/null +++ b/lib/coq/list/Mem.v @@ -0,0 +1,30 @@ +(* This file is generated by Why3's Coq-realize driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require list.List. + +(* Why3 assumption *) +Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop := + match l with + | nil => False + | (cons y r) => (x = y) \/ (mem x r) + end. + + +Lemma mem_std : + forall {a:Type} {a_WT:WhyType a} (x:a) (l:list a), + mem x l <-> List.In x l. +Proof. +intros a a_WT x l. +induction l as [|h q]. +easy. +simpl. +split ; intros [H|H]. +now left. +right. +now apply IHq. +now left. +right. +now apply IHq. +Qed. diff --git a/lib/coq/list/Nth.v b/lib/coq/list/Nth.v index 2c76f1188..4ef55132b 100644 --- a/lib/coq/list/Nth.v +++ b/lib/coq/list/Nth.v @@ -7,13 +7,14 @@ Require list.List. Require option.Option. (* Why3 goal *) -Definition nth: forall {a:Type} {a_WT:WhyType a}, Z -> list a -> option a. +Definition nth: forall {a:Type} {a_WT:WhyType a}, Z -> (list a) + -> (option a). intros a a_WT. exact (fix nth n l := match l with nil => None | cons h t => if Zeq_bool n Z0 then Some h else nth (n - 1)%Z t end). Defined. (* Why3 goal *) -Lemma nth_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (l:list a), +Lemma nth_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (l:(list a)), match l with | nil => ((nth n l) = None) | (cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) -> diff --git a/lib/coq/list/NthHdTl.v b/lib/coq/list/NthHdTl.v new file mode 100644 index 000000000..37b2f40a9 --- /dev/null +++ b/lib/coq/list/NthHdTl.v @@ -0,0 +1,37 @@ +(* 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. + +(* Why3 goal *) +Lemma Nth_tl : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)), ((list.HdTl.tl l1) = (Some l2)) -> forall (i:Z), + (~ (i = (-1%Z)%Z)) -> ((list.Nth.nth i l2) = (list.Nth.nth (i + 1%Z)%Z + l1)). +Proof. +intros a a_WT [|x1 l1] l2 h1 i h2. +easy. +simpl. +generalize (Zeq_bool_if (i + 1) 0). +case Zeq_bool. +omega. +intros _. +simpl in h1. +inversion h1. +apply (f_equal (fun i => Nth.nth i l2)). +exact (Zpred_succ i). +Qed. + +(* Why3 goal *) +Lemma Nth0_head : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + ((list.Nth.nth 0%Z l) = (list.HdTl.hd l)). +Proof. +now intros a a_WT [|h t]. +Qed. + + diff --git a/lib/coq/list/NthLength.v b/lib/coq/list/NthLength.v index 2cab6d394..b68901588 100644 --- a/lib/coq/list/NthLength.v +++ b/lib/coq/list/NthLength.v @@ -9,8 +9,8 @@ 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). +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]. @@ -27,8 +27,8 @@ 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). +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]. @@ -49,8 +49,8 @@ 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 \/ +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. diff --git a/theories/list.why b/theories/list.why index baa791321..1b7abd02d 100644 --- a/theories/list.why +++ b/theories/list.why @@ -118,7 +118,7 @@ theory NthHdTl lemma Nth_tl: forall l1 l2: list 'a. tl l1 = Some l2 -> - forall i: int. nth i l2 = nth (i+1) l1 + forall i: int. i <> -1 -> nth i l2 = nth (i+1) l1 lemma Nth0_head: forall l: list 'a. nth 0 l = hd l -- GitLab