more theory for lists

diff --git a/helm/software/matita/nlibrary/datatypes/list.ma b/helm/software/matita/nlibrary/datatypes/list.ma
index 2909baf84bc543dc373b11e7f02e078adfd7bbb4..87f91718526c1384736c4015e4f42e535a9f7acc 100644 (file)
--- a/helm/software/matita/nlibrary/datatypes/list.ma
+++ b/helm/software/matita/nlibrary/datatypes/list.ma
@@ -13,6 +13,8 @@
 (**************************************************************************)
 
 include "logic/pts.ma".
+include "logic/equality.ma".
+include "arithmetics/nat.ma".
 
 ninductive list (A:Type[0]) : Type[0] ≝ 
   | nil: list A
@@ -56,7 +58,8 @@ match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
 
 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
 #A;#l;nelim l;//;
-#a;#l1;#IH;nnormalize;//;
+#a;#l1;#IH;nnormalize;
+nrewrite > IH;//;
 nqed.
 
 ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
@@ -187,18 +190,20 @@ interpretation "list member" 'mem x l = (in_list ? x l).
 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
   
-naxiom not_in_list_nil : \forall A,x.\lnot in_list A x [].
-(*intros.unfold.intro.inversion H
-  [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
-  |intros;destruct H4]
-qed.*)
+nlemma not_in_list_nil : \forall A,x.\lnot in_list A x [].
+#A x;@;#H1;ninversion H1;
+##[#a0 al0 H2 H3;ndestruct (H3);
+##|#a0 a1 al0 H2 H3 H4 H5;ndestruct (H5)
+##]
+nqed.
 
-naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
+nlemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
                           x = a \lor in_list A x l.
-(*intros;inversion H;intros
-  [destruct H2;left;reflexivity
-  |destruct H4;right;assumption]
-qed.*)
+#A a0 a1 al0 H1;ninversion H1
+##[#a2 al1 H2 H3;ndestruct (H3);@;@
+##|#a2 a3 al1 H2 H3 H4 H5;ndestruct (H5);@2;//
+##]
+nqed.
 
 nlemma in_list_tail : \forall A,l,x,y.
       in_list A x (y::l) \to x \neq y \to in_list A x l.
@@ -210,45 +215,43 @@ ninversion H;
 ##]
 nqed.
 
-naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
-(*intros;elim (in_list_cons_case ? ? ? ? H)
-  [assumption
-  |elim (not_in_list_nil ? ? H1)]
-qed.*)
+nlemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
+#A a0 a1 H1;ncases (in_list_cons_case ???? H1)
+##[//
+##|#H2;napply False_ind;ncases (not_in_list_nil ? a0);#H3;/2/
+##]
+nqed.
 
-naxiom in_list_to_in_list_append_l: \forall A.\forall x:A.
+nlemma in_list_to_in_list_append_l: \forall A.\forall x:A.
 \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
-(*intros.
-elim H;simplify
-  [apply in_list_head
-  |apply in_list_cons;assumption
-  ]
-qed.*)
-
-naxiom in_list_to_in_list_append_r: \forall A.\forall x:A.
+#A a0 al0 al1 H1;nelim H1
+##[#a1 al2;@;
+##|#a1 a2 al2 H2 H3;@2;//
+##]
+nqed.
+
+nlemma in_list_to_in_list_append_r: \forall A.\forall x:A.
 \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
-(*intros 3.
-elim l1;simplify
-  [assumption
-  |apply in_list_cons;apply H;assumption
-  ]
-qed.*)
-
-naxiom in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
+#A a0 al0 al1 H1;nelim al0
+##[napply H1
+##|#a1 al2 IH;@2;napply IH
+##]
+nqed.
+
+nlemma in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
 \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
-(*intros 3.
-elim l
-  [right.apply H
-  |simplify in H1.inversion H1;intros; destruct;
-    [left.apply in_list_head
-    | elim (H l2)
-      [left.apply in_list_cons. assumption
-      |right.assumption
-      |assumption
-      ]
-    ]
-  ]
-qed.*)
+#A a0 al0;nelim al0
+##[#al1 H1;@2;napply H1
+##|#a1 al1 IH al2 H1;nnormalize in H1;
+   ncases (in_list_cons_case ???? H1);#H2
+   ##[@;nrewrite > H2;@
+   ##|ncases (IH … H2);#H3
+      ##[@;@2;//
+      ##|@2;//
+      ##]
+   ##]
+##]
+nqed.
 
 nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
  match l with
@@ -260,78 +263,92 @@ nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
      ]
   ].
   
-naxiom mem_true_to_in_list :
+nlemma mem_true_to_in_list :
   \forall A,equ.
   (\forall x,y.equ x y = true \to x = y) \to
   \forall x,l.mem A equ x l = true \to in_list A x l.
-(* intros 5.elim l
-  [simplify in H1;destruct H1
-  |simplify in H2;apply (bool_elim ? (equ x a))
-     [intro;rewrite > (H ? ? H3);apply in_list_head
-     |intro;rewrite > H3 in H2;simplify in H2;
-      apply in_list_cons;apply H1;assumption]]
-qed.*)
-
-naxiom in_list_to_mem_true :
+#A equ H1 a0 al0;nelim al0
+##[nnormalize;#H2;ndestruct (H2)
+##|#a1 al1 IH H2;nwhd in H2:(??%?);
+   nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3
+   ##[nrewrite > (H1 … H3);@
+   ##|@2;napply IH;nrewrite > H3 in H2;nnormalize;//;
+   ##]
+##]
+nqed.
+
+nlemma in_list_to_mem_true :
   \forall A,equ.
   (\forall x.equ x x = true) \to
   \forall x,l.in_list A x l \to mem A equ x l = true.
-(*intros 5.elim l
-  [elim (not_in_list_nil ? ? H1)
-  |elim H2
-    [simplify;rewrite > H;reflexivity
-    |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
-qed.*)
-
-naxiom in_list_filter_to_p_true : \forall A,l,x,p.
+#A equ H1 a0 al0;nelim al0
+##[#H2;napply False_ind;ncases (not_in_list_nil ? a0);/2/
+##|#a1 al1 IH H2;nelim H2
+   ##[nnormalize;#a2 al2;nrewrite > (H1 …);@
+   ##|#a2 a3 al2 H3 H4;nnormalize;ncases (equ a2 a3);nnormalize;//;
+   ##]
+##]
+nqed.
+
+nlemma in_list_filter_to_p_true : \forall A,l,x,p.
 in_list A x (filter A l p) \to p x = true.
-(* intros 4;elim l
-  [simplify in H;elim (not_in_list_nil ? ? H)
-  |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
-   simplify in H1
-     [elim (in_list_cons_case ? ? ? ? H1)
-        [rewrite > H3;assumption
-        |apply (H H3)]
-     |apply (H H1)]]
-qed.*)
-
-naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
-(*intros 4;elim l
-  [simplify in H;elim (not_in_list_nil ? ? H)
-  |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
-   simplify in H1
-     [elim (in_list_cons_case ? ? ? ? H1)
-        [rewrite > H3;apply in_list_head
-        |apply in_list_cons;apply H;assumption]
-     |apply in_list_cons;apply H;assumption]]
-qed.*)
-
-naxiom in_list_filter_r : \forall A,l,p,x.
+#A al0 a0 p;nelim al0
+##[nnormalize;#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
+##|#a1 al1 IH H1;nnormalize in H1;nlapply (refl ? (p a1));
+   ngeneralize in match H1;ncases (p a1) in ⊢ (???% -> ???% → %);
+   ##[#H2 H3;ncases (in_list_cons_case ???? H2);#H4
+      ##[nrewrite > H4;//
+      ##|napply (IH H4);
+      ##]
+   ##|#H2 H3;napply (IH H2);
+   ##]
+##]
+nqed.
+
+nlemma in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
+#A al0 p a0;nelim al0
+##[nnormalize;//;
+##|#a1 al1 IH H1;nnormalize in H1;
+   nlapply (refl ? (p a1));ncases (p a1) in ⊢ (???% → %);#H2
+   ##[nrewrite > H2 in H1;#H1;ncases (in_list_cons_case ???? H1);#H3
+      ##[nrewrite > H3;@
+      ##|@2;napply IH;napply H3
+      ##]
+   ##|@2;napply IH;nrewrite > H2 in H1;#H1;napply H1;
+   ##]
+##]
+nqed.
+
+nlemma in_list_filter_r : \forall A,l,p,x.
               in_list A x l \to p x = true \to in_list A x (filter A l p).
-(* intros 4;elim l
-  [elim (not_in_list_nil ? ? H)
-  |elim (in_list_cons_case ? ? ? ? H1)
-     [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
-     |simplify;apply (bool_elim ? (p a));intro;simplify;
-        [apply in_list_cons;apply H;assumption
-        |apply H;assumption]]]
-qed.*)
-
-naxiom incl_A_A: ∀T,A.incl T A A.
-(*intros.unfold incl.intros.assumption.
-qed.*)
-
-naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
-(*unfold incl; intros;autobatch.
-qed.*)
-
-naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
-(*unfold incl; intros;autobatch.
-qed.*)
-
-naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
-(*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
-qed.*)
+#A al0 p a0;nelim al0
+##[#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
+##|#a1 al1 IH H1 H2;ncases (in_list_cons_case ???? H1);#H3
+   ##[nnormalize;nrewrite < H3;nrewrite > H2;@
+   ##|nnormalize;ncases (p a1);nnormalize;
+      ##[@2;napply IH;//
+      ##|napply IH;//
+      ##]
+   ##]
+##]
+nqed.
+   
+nlemma incl_A_A: ∀T,A.incl T A A.
+#A al0 a0 H1;//;
+nqed.
+
+nlemma incl_append_l : ∀T,A,B.incl T A (A @ B).
+#A al0 al1 a0 H1;/2/;
+nqed.
+
+nlemma incl_append_r : ∀T,A,B.incl T B (A @ B).
+#A al0 al1 a0 H1;/2/;
+nqed.
+
+nlemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
+#A al0 al1 a0 H1 a1 H2;ncases (in_list_cons_case ???? H2);/2/;
+#H3;@2;napply H1;//;
+nqed.
 
 nlet rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l ≝ 
  match l with
@@ -443,15 +460,37 @@ nlemma map_compose :
 ##]
 nqed.
 
-naxiom incl_incl_to_incl_append : 
+nlemma incl_incl_to_incl_append : 
   ∀A.∀l1,l2,l1',l2':list A.l1 ⊆ l1' → l2 ⊆ l2' → l1@l2 ⊆ l1'@l2'.
+#A al0 al1 al2 al3 H1 H2 a0 H3;
+ncases (in_list_append_to_or_in_list ???? H3);#H4;
+##[napply in_list_to_in_list_append_l;napply H1;//
+##|napply in_list_to_in_list_append_r;napply H2;//
+##]
+nqed.
   
-naxiom eq_map_append : ∀A,B,f,l1,l2.map A B f (l1@l2) = map A B f l1@map A B f l2.  
+nlemma eq_map_append : 
+  ∀A,B,f,l1,l2.map A B f (l1@l2) = map A B f l1@map A B f l2.
+#A B f al1 al2;nelim al1
+##[@
+##|#a0 al3 IH;nnormalize;nrewrite > IH;@;
+##]
+nqed.
 
-naxiom not_in_list_to_mem_false :
+nlemma not_in_list_to_mem_false :
   ∀A,equ.
   (∀x,y.equ x y = true → x = y) →
   ∀x:A.∀l. x ∉ l → mem A equ x l = false.
+#A equ H1 a0 al0;nelim al0
+##[#_;@
+##|#a1 al1 IH H2;nwhd in ⊢ (??%?);
+   nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3;
+   ##[napply False_ind;ncases H2;#H4;napply H4;
+      nrewrite > (H1 … H3);@
+   ##|napply IH;@;#H4;ncases H2;#H5;napply H5;@2;//
+   ##]
+##]
+nqed.
 
 nlet rec list_forall (A:Type[0]) (l:list A) (p:A → bool) on l : bool ≝ 
  match l with