Decidability of equality (draft)

[helm.git] / weblib / basics / list.ma

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 798f5762933b3fd9c1d2153761e08d33e31dc689..7d0c2ba13f2da25c065da05a332f3a7a8ba5bf49 100644 (file)
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -9,8 +9,8 @@
      \ /   GNU General Public License Version 2   
       V_______________________________________________________________ *)
 
-include "basics/types.ma".
-include "arithmetics/nat.ma".
+include "basics/bool.ma".
+(* include "arithmetics/nat.ma". *)
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
@@ -72,7 +72,7 @@ ntheorem cons_append_commute:
 //; nqed. *)
 
 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-/2/ qed.
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace trans_eq\ 5/span\ 6\ 5/span\ 6/ qed.
 
 theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. 
   l1@l2=[] → P (nil A) (nil A) → P l1 l2.
@@ -82,7 +82,7 @@ qed.
 
 theorem nil_to_nil:  ∀A.∀l1,l2:list A.
   l1@l2 = [] → l1 = [] ∧ l2 = [].
-#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
+#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace conj\ 5/span\ 6\ 5/span\ 6/
 qed.
 
 (* iterators *)
@@ -108,13 +108,14 @@ lemma filter_false : ∀A,l,a,p. p a = false →
 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
+(*
 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
 match l1 with
-  [ nil ⇒ nil ?
+  [ nil ⇒ nil ?  
   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
-  ].
+  ]. *)
 
-(**************************** length ******************************)
+(**************************** length ******************************
 
 let rec length (A:Type[0]) (l:list A) on l ≝ 
   match l with 
@@ -129,7 +130,7 @@ let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝
     [O ⇒ hd A l d
     |S m ⇒ nth m A (tail A l) d].
 
-(**************************** fold *******************************)
+**************************** fold *******************************)
 
 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝  
  match l with 
@@ -181,5 +182,4 @@ theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
     \fold[op,nil]_{i∈(I@J)} (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
   [>nill //|#a #tl #Hind <assoc //]
-qed.
-
+qed.
\ No newline at end of file