Realize some more theories about lists. Fix an inconsistent axiom along the way.

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

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)"
 

lib/coq/list/Append.v

+(* 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.
+
+

lib/coq/list/HdTl.v

+(* 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.
+
+

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.

lib/coq/list/Mem.v

+(* 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.

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)) ->

lib/coq/list/NthHdTl.v

+(* 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.
+
+

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.

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