(\exists B,T.(in_list ? (mk_bound B x T) G)) \to
(in_list ? x (fv_env G)).
intros 2;elim G
- [elim H;elim H1;lapply (in_list_nil ? ? H2);elim Hletin
- |elim H1;elim H2;elim (in_cons_case ? ? ? ? H3)
- [rewrite < H4;simplify;apply in_Base
- |simplify;apply in_Skip;apply H;apply (ex_intro ? ? a);
+ [elim H;elim H1;lapply (not_in_list_nil ? ? H2);elim Hletin
+ |elim H1;elim H2;elim (in_list_cons_case ? ? ? ? H3)
+ [rewrite < H4;simplify;apply in_list_head
+ |simplify;apply in_list_cons;apply H;apply (ex_intro ? ? a);
apply (ex_intro ? ? a1);assumption]]
qed.
lemma natinfv_boundinenv : \forall x,G.(in_list ? x (fv_env G)) \to
\exists B,T.(in_list ? (mk_bound B x T) G).
intros 2;elim G 0
- [simplify;intro;lapply (in_list_nil ? ? H);elim Hletin
- |intros 3;elim t;simplify in H1;elim (in_cons_case ? ? ? ? H1)
- [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_Base
+ [simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin
+ |intros 3;elim t;simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+ [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_list_head
|elim (H H2);elim H3;apply (ex_intro ? ? a);
- apply (ex_intro ? ? a1);apply in_Skip;assumption]]
+ apply (ex_intro ? ? a1);apply in_list_cons;assumption]]
qed.
lemma incl_bound_fv : \forall l1,l2.(incl ? l1 l2) \to
lemma incl_cons : \forall x,l1,l2.
(incl ? l1 l2) \to (incl nat (x :: l1) (x :: l2)).
-intros.unfold in H.unfold.intros.elim (in_cons_case ? ? ? ? H1)
- [rewrite > H2;apply in_Base|apply in_Skip;apply (H ? H2)]
+intros.unfold in H.unfold.intros.elim (in_list_cons_case ? ? ? ? H1)
+ [rewrite > H2;apply in_list_head|apply in_list_cons;apply (H ? H2)]
qed.
lemma WFT_env_incl : \forall G,T.(WFType G T) \to
(y \neq x) \to
(in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))).
intros 10;elim H
- [simplify in H1;elim (in_cons_case ? ? ? ? H1)
+ [simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
[destruct H3;elim (H2);reflexivity
- |simplify;apply (in_Skip ? ? ? ? H3);]
- |simplify in H2;simplify;elim (in_cons_case ? ? ? ? H2)
- [rewrite > H4;apply in_Base
- |apply (in_Skip ? ? ? ? (H1 H4 H3))]]
+ |simplify;apply (in_list_cons ? ? ? ? H3);]
+ |simplify in H2;simplify;elim (in_list_cons_case ? ? ? ? H2)
+ [rewrite > H4;apply in_list_head
+ |apply (in_list_cons ? ? ? ? (H1 H4 H3))]]
qed.
lemma in_FV_subst : \forall x,T,U,n.(in_list ? x (fv_type T)) \to
(in_list ? x (fv_type (subst_type_nat T U n))).
intros 3;elim T
- [simplify in H;elim (in_list_nil ? ? H)
+ [simplify in H;elim (not_in_list_nil ? ? H)
|2,3:simplify;simplify in H;assumption
- |*:simplify in H2;simplify;elim (append_to_or_in_list ? ? ? ? H2)
- [1,3:apply in_list_append1;apply (H ? H3)
- |*:apply in_list_append2;apply (H1 ? H3)]]
+ |*:simplify in H2;simplify;elim (in_list_append_to_or_in_list ? ? ? ? H2)
+ [1,3:apply in_list_to_in_list_append_l;apply (H ? H3)
+ |*:apply in_list_to_in_list_append_r;apply (H1 ? H3)]]
qed.
(*** lemma on fresh names ***)
[apply a
|apply H;constructor 1]
|intros;elim l
- [apply (ex_intro ? ? O);intros;unfold;intro;elim (in_list_nil ? ? H1)
+ [apply (ex_intro ? ? O);intros;unfold;intro;elim (not_in_list_nil ? ? H1)
|elim H;
apply (ex_intro ? ? (S (max a t))).
intros.unfold. intro.
- elim (in_cons_case ? ? ? ? H3)
+ elim (in_list_cons_case ? ? ? ? H3)
[rewrite > H4 in H2.autobatch
|elim H4
[apply (H1 m ? H4).apply (trans_le ? (max a t));autobatch
lemma fv_WFT : \forall T,x,G.(WFType G T) \to (in_list ? x (fv_type T)) \to
(in_list ? x (fv_env G)).
intros 4.elim H
- [simplify in H2;elim (in_cons_case ? ? ? ? H2)
- [rewrite > H3;assumption|elim (in_list_nil ? ? H3)]
- |simplify in H1;elim (in_list_nil ? x H1)
- |simplify in H5;elim (append_to_or_in_list ? ? ? ? H5);autobatch
- |simplify in H5;elim (append_to_or_in_list ? ? ? ? H5)
+ [simplify in H2;elim (in_list_cons_case ? ? ? ? H2)
+ [rewrite > H3;assumption|elim (not_in_list_nil ? ? H3)]
+ |simplify in H1;elim (not_in_list_nil ? x H1)
+ |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch
+ |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5)
[apply (H2 H6)
|elim (fresh_name ((fv_type t1) @ (fv_env l)));
cut (¬ (a ∈ (fv_type t1)) ∧ ¬ (a ∈ (fv_env l)))
[elim Hcut;lapply (H4 ? H9 H8)
[cut (x ≠ a)
- [simplify in Hletin;elim (in_cons_case ? ? ? ? Hletin)
+ [simplify in Hletin;elim (in_list_cons_case ? ? ? ? Hletin)
[elim (Hcut1 H10)
|assumption]
|intro;apply H8;applyS H6]
|apply in_FV_subst;assumption]
|split
- [intro;apply H7;apply in_list_append1;assumption
- |intro;apply H7;apply in_list_append2;assumption]]]]
+ [intro;apply H7;apply in_list_to_in_list_append_l;assumption
+ |intro;apply H7;apply in_list_to_in_list_append_r;assumption]]]]
qed.
(*** lemmata relating subtyping and well-formedness ***)
(in_list ? (mk_bound B x T) G) \to
(in_list ? (mk_bound B x U) G) \to T = U.
intros 6;elim H
- [lapply (in_list_nil ? ? H1);elim Hletin
- |elim (in_cons_case ? ? ? ? H6)
- [destruct H7;destruct;elim (in_cons_case ? ? ? ? H5)
+ [lapply (not_in_list_nil ? ? H1);elim Hletin
+ |elim (in_list_cons_case ? ? ? ? H6)
+ [destruct H7;destruct;elim (in_list_cons_case ? ? ? ? H5)
[destruct H7;reflexivity
|elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B);
apply (ex_intro ? ? T);assumption]
- |elim (in_cons_case ? ? ? ? H5)
+ |elim (in_list_cons_case ? ? ? ? H5)
[destruct H8;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B);
apply (ex_intro ? ? U);assumption
|apply (H2 H8 H7)]]]
[unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9)
|apply (WFE_cons ? ? ? ? H6 H8);autobatch
|unfold;intros;inversion H9;intros
- [destruct H11;apply in_Base
- |destruct H13;apply in_Skip;apply (H7 ? H10)]]]
+ [destruct H11;apply in_list_head
+ |destruct H13;apply in_list_cons;apply (H7 ? H10)]]]
qed.
theorem narrowing:∀X,G,G1,U,P,M,N.
[unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9)
|apply (WFE_cons ? ? ? ? H6 H8);autobatch
|unfold;intros;inversion H9;intros
- [destruct H11;apply in_Base
- |destruct H13;apply in_Skip;apply (H7 ? H10)]]]
+ [destruct H11;apply in_list_head
+ |destruct H13;apply in_list_cons;apply (H7 ? H10)]]]
qed.
theorem narrowing:∀X,G,G1,U,P,M,N.
include "logic/equality.ma".
include "nat/compare.ma".
include "list/list.ma".
+include "list/in.ma".
(*** useful definitions and lemmas not really related to Fsub ***)
]
qed.
-inductive in_list (A:Type): A → (list A) → Prop ≝
-| in_Base : ∀ x,l.(in_list A x (x::l))
-| in_Skip : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
-
notation > "hvbox(x ∈ l)"
non associative with precedence 30 for @{ 'inlist $x $l }.
notation < "hvbox(x \nbsp ∈ \nbsp l)"
non associative with precedence 30 for @{ 'inlist $x $l }.
interpretation "item in list" 'inlist x l =
- (cic:/matita/Fsub/util/in_list.ind#xpointer(1/1) _ x l).
-
-definition incl : \forall A.(list A) \to (list A) \to Prop \def
- \lambda A,l,m.\forall x.(in_list A x l) \to (in_list A x m).
-
-(* FIXME: use the map in library/list (when there will be one) *)
-definition map : \forall A,B,f.((list A) \to (list B)) \def
- \lambda A,B,f.let rec map (l : (list A)) : (list B) \def
- match l in list return \lambda l0:(list A).(list B) with
- [nil \Rightarrow (nil B)
- |(cons (a:A) (t:(list A))) \Rightarrow
- (cons B (f a) (map t))] in map.
-
-lemma 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.
-
-lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ∈ t).
-intros;inversion H;intros
- [destruct H2;left;symmetry;reflexivity
- |destruct H4;right;applyS H1]
-qed.
-
-lemma append_nil:\forall A:Type.\forall l:list A. l@[]=l.
-intros.
-elim l;intros;autobatch.
-qed.
-
-lemma append_cons:\forall A.\forall a:A.\forall l,l1.
-l@(a::l1)=(l@[a])@l1.
-intros.
-rewrite > associative_append.
-reflexivity.
-qed.
-
-lemma in_list_append1: \forall A.\forall x:A.
-\forall l1,l2. x \in l1 \to x \in l1@l2.
-intros.
-elim H
- [simplify.apply in_Base
- |simplify.apply in_Skip.assumption
- ]
-qed.
-
-lemma in_list_append2: \forall A.\forall x:A.
-\forall l1,l2. x \in l2 \to x \in l1@l2.
-intros 3.
-elim l1
- [simplify.assumption
- |simplify.apply in_Skip.apply H.assumption
- ]
-qed.
-
-theorem append_to_or_in_list: \forall A:Type.\forall x:A.
-\forall l,l1. x \in l@l1 \to (x \in l) \lor (x \in l1).
-intros 3.
-elim l
- [right.apply H
- |simplify in H1.inversion H1;intros; destruct;
- [left.apply in_Base
- | elim (H l2)
- [left.apply in_Skip. assumption
- |right.assumption
- |assumption
- ]
- ]
- ]
-qed.
+ (cic:/matita/list/in/in_list.ind#xpointer(1/1) _ x l).
lemma max_case : \forall m,n.(max m n) = match (leb m n) with
[ true \Rightarrow n
| false \Rightarrow m ].
intros;elim m;simplify;reflexivity;
-qed.
-
-lemma incl_A_A: ∀T,A.incl T A A.
-intros.unfold incl.intros.assumption.
qed.
\ No newline at end of file
include "decidable_kit/eqtype.ma".
include "nat/plus.ma".
-(* ### some functions on lists (some can be moved to list.ma ### *)
-
-let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B :=
- match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)].
-
-definition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l.
+(* ### some functions on lists ### *)
definition count : ∀T : eqType.∀f : T → bool.∀l : list T. nat :=
λT:eqType.λf,l.
[ nil ⇒ false
| cons y tl ⇒ orb (cmp d x y) (mem d x tl)].
-definition iota : nat → nat → list nat ≝
- λn,m. nat_rect (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
-
-let rec map (A,B:Type) (f: A → B) (l : list A) on l : list B ≝
- match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
-
-(* ### induction principle for functions visiting 2 lists in parallel *)
-lemma list_ind2 :
- ∀T1,T2:Type.∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
- length ? l1 = length ? l2 →
- (P (nil ?) (nil ?)) →
- (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
- P l1 l2.
-intros (T1 T2 l1 l2 P Hl Pnil Pcons);
-generalize in match Hl; clear Hl; generalize in match l2; clear l2;
-elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| simplify in Hl; destruct Hl]]
-intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl]
-intros 1 (Hl); apply Pcons; apply IH; simplify in Hl; destruct Hl; assumption;
-qed.
-
-lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
-intros (A B f g l Efg); elim l; simplify; [1: reflexivity ];
-rewrite > (Efg t); rewrite > H; reflexivity;
-qed.
-
(* ### eqtype for lists ### *)
let rec lcmp (d : eqType) (l1,l2 : list d) on l1 : bool ≝
match l1 with
apply H'; reflexivity;]]]]
qed.
-definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).
-
\ No newline at end of file
+definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "datatypes/bool.ma".
+include "datatypes/constructors.ma".
+include "list/list.ma".
+
+inductive in_list (A:Type): A → (list A) → Prop ≝
+| in_list_head : ∀ x,l.(in_list A x (x::l))
+| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
+
+definition incl : \forall A.(list A) \to (list A) \to Prop \def
+ \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
+
+lemma 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.
+
+lemma 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.
+
+lemma in_list_tail : \forall l,x,y.
+ in_list nat x (y::l) \to x \neq y \to in_list nat x l.
+intros 4;elim (in_list_cons_case ? ? ? ? H)
+ [elim (H2 H1)
+ |assumption]
+qed.
+
+lemma 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.
+
+lemma 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.
+
+lemma 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.
+
+theorem 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.
+
+let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
+ match l with
+ [ nil ⇒ false
+ | (cons a l') ⇒
+ match eq x a with
+ [ true ⇒ true
+ | false ⇒ mem A eq x l'
+ ]
+ ].
+
+lemma 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 t))
+ [intro;rewrite > (H ? ? H3);apply in_list_head
+ |intro;rewrite > H3 in H2;simplify in H2;
+ apply in_list_cons;apply H1;assumption]]
+qed.
+
+lemma 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 a a1));intro;rewrite > H5;
+ reflexivity]].
+qed.
+
+lemma in_list_filter_to_p_true : \forall l,x,p.
+in_list nat x (filter nat l p) \to p x = true.
+intros 3;elim l
+ [simplify in H;elim (not_in_list_nil ? ? H)
+ |simplify in H1;apply (bool_elim ? (p t));intro;rewrite > H2 in H1;
+ simplify in H1
+ [elim (in_list_cons_case ? ? ? ? H1)
+ [rewrite > H3;assumption
+ |apply (H H3)]
+ |apply (H H1)]]
+qed.
+
+lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
+intros 3;elim l
+ [simplify in H;elim (not_in_list_nil ? ? H)
+ |simplify in H1;apply (bool_elim ? (p t));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.
+
+lemma in_list_filter_r : \forall l,p,x.
+ in_list nat x l \to p x = true \to in_list nat x (filter nat l p).
+intros 3;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 t));intro;rewrite > H4;simplify
+ [apply in_list_cons;apply H;assumption
+ |apply H;assumption]]]
+qed.
+
+lemma incl_A_A: ∀T,A.incl T A A.
+intros.unfold incl.intros.assumption.
+qed.
\ No newline at end of file
set "baseuri" "cic:/matita/list/".
include "logic/equality.ma".
+include "datatypes/bool.ma".
include "higher_order_defs/functions.ma".
+include "nat/plus.ma".
+include "nat/orders.ma".
inductive list (A:Type) : Type :=
| nil: list A
reflexivity;
qed.
+lemma append_cons:\forall A.\forall a:A.\forall l,l1.
+l@(a::l1)=(l@[a])@l1.
+intros.
+rewrite > associative_append.
+reflexivity.
+qed.
+
inductive permutation (A:Type) : list A -> list A -> Prop \def
| refl : \forall l:list A. permutation ? l l
| swap : \forall l:list A. \forall x,y:A.
]
| S n' ⇒ nth A (tail ? l) d n'
].
+
+let rec map (A,B:Type) (f: A → B) (l : list A) on l : list B ≝
+ match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+
+let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B :=
+ match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)].
+
+definition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l.
+
+definition filter \def
+ \lambda T:Type.\lambda l:list T.\lambda p:T \to bool.
+ foldr T (list T)
+ (\lambda x,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
+
+definition iota : nat → nat → list nat ≝
+ λn,m. nat_rect (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
+
+(* ### induction principle for functions visiting 2 lists in parallel *)
+lemma list_ind2 :
+ ∀T1,T2:Type.∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
+ length ? l1 = length ? l2 →
+ (P (nil ?) (nil ?)) →
+ (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
+ P l1 l2.
+intros (T1 T2 l1 l2 P Hl Pnil Pcons);
+generalize in match Hl; clear Hl; generalize in match l2; clear l2;
+elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| simplify in Hl; destruct Hl]]
+intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl]
+intros 1 (Hl); apply Pcons; apply IH; simplify in Hl; destruct Hl; assumption;
+qed.
+
+lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+intros (A B f g l Efg); elim l; simplify; [1: reflexivity ];
+rewrite > (Efg t); rewrite > H; reflexivity;
+qed.
+
+lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l.
+intros;elim l
+ [simplify;apply le_n
+ |simplify;apply (bool_elim ? (p t));intro
+ [simplify;apply le_S_S;assumption
+ |simplify;apply le_S;assumption]]
+qed.
\ No newline at end of file
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/list/sort/".
-
include "datatypes/bool.ma".
include "datatypes/constructors.ma".
-include "list/list.ma".
+include "list/in.ma".
+
+inductive sorted (A:Type) (P:A \to A \to Prop): list A \to Prop \def
+| sort_nil : sorted A P []
+| sort_cons : \forall x,l.sorted A P l \to (\forall y.in_list ? y l \to P x y)
+ \to sorted A P (x::l).
+
+lemma sorted_cons_to_sorted : \forall A,P,x,l.sorted A P (x::l) \to sorted A P l.
+intros;inversion H;intros
+ [destruct H1
+ |destruct H4;assumption]
+qed.
+
+lemma sorted_to_minimum : \forall A,P,x,l.sorted A P (x::l) \to
+ \forall y.in_list ? y l \to P x y.
+intros;inversion H;intros;
+ [destruct H2
+ |destruct H5;apply H4;assumption]
+qed.
+
-let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
- match l with
- [ nil ⇒ false
- | (cons a l') ⇒
- match eq x a with
- [ true ⇒ true
- | false ⇒ mem A eq x l'
- ]
- ].
-
let rec ordered (A:Type) (le: A → A → bool) (l: list A) on l ≝
match l with
[ nil ⇒ true
]
].
+lemma sorted_to_eq_sorted_b_true :
+ \forall A,ord,ordb.
+ (\forall x,y.ord x y \to ordb x y = true) \to
+ \forall l.sorted A ord l \to ordered A ordb l = true.
+intros 5;elim l
+ [reflexivity
+ |simplify;rewrite > H1;generalize in match H2;cases l1;intros
+ [reflexivity
+ |simplify;rewrite > H
+ [reflexivity
+ |apply (sorted_to_minimum ? ? ? ? H3);apply in_list_head]
+ |apply sort_nil
+ |apply (sorted_cons_to_sorted ? ? ? ? H3)]]
+qed.
+
+(*
+ TODO
+ per far funzionare questa dimostrazione bisogna appoggiarsi a un
+ eqb (e utilizzare quindi in_list <-> mem), oppure modificare la definizione
+ di sorted in modo che non si appoggi più a in_list:
+ sorted []
+ sorted [x] per ogni x
+ sorted x::y::l se ord x y e sorted y::l
+
+lemma eq_sorted_b_true_to_sorted :
+ \forall A,ord,ordb.
+ (\forall x,y.ordb x y = true \to ord x y) \to
+ \forall l.ordered A ordb l = true \to sorted A ord l.
+intros 5;elim l
+ [apply sort_nil
+ |apply sort_cons
+ [apply H1;simplify in H2;generalize in match H2;cases l1;intros
+ [reflexivity
+ |simplify in H3;simplify;apply (andb_true_true_r ? ? H3)]
+ |intros;apply H;generalize in match H2;
+ generalize in match (in_list_to_mem_true ? ? ? ? H
+ [
+*)
+
let rec insert (A:Type) (le: A → A → bool) x (l: list A) on l ≝
match l with
[ nil ⇒ [x]
include "nat/sqrt.ma".
include "nat/chebyshev_teta.ma".
include "nat/chebyshev.ma".
-include "list/list.ma".
+include "list/in.ma".
+include "list/sort.ma".
include "nat/o.ma".
let rec list_divides l n \def
| false => aux m1 (n-m1::acc)]]
in aux (pred n) [].
-let rec filter A l p on l \def
- match l with
- [ nil => nil A
- | cons (a:A) (tl:list A) => match (p a) with
- [ true => a::(filter A tl p)
- | false => filter A tl p ]].
-
-let rec length A (l:list A) on l \def
- match l with
- [ nil => O
- | cons (a:A) (tl:list A) => S (length A tl) ].
-
let rec list_n_aux n k \def
match n with
[ O => nil nat
definition sieve : nat \to list nat \def
\lambda m.sieve_aux [] (list_n m) m.
-definition ord_list \def
- \lambda l.
- \forall a,b,l1,l2.l = l1@(a::b::l2) \to b \leq a.
-
-definition in_list \def
- \lambda A.\lambda a:A.\lambda l:list A.
- \exists l1,l2.l = l1@(a::l2).
-
-lemma in_list_filter_to_p_true : \forall l,x,p.
-in_list nat x (filter nat l p) \to p x = true.
-intros;elim H;elim H1;clear H H1;generalize in match H2;generalize in match a;elim l 0
- [simplify;intro;elim l1
- [simplify in H;destruct H
- |simplify in H1;destruct H1]
- |intros;simplify in H1;apply (bool_elim ? (p t));intro;
- rewrite > H3 in H1;simplify in H1
- [generalize in match H1;elim l2
- [simplify in H4;destruct H4;assumption
- |simplify in H5;destruct H5;apply (H l3);assumption]
- |apply (H l2);assumption]]
-qed.
-
-lemma in_list_cons : \forall l,x,y.in_list nat x l \to in_list nat x (y::l).
-intros;unfold in H;unfold;elim H;elim H1;apply (ex_intro ? ? (y::a));
-apply (ex_intro ? ? a1);simplify;rewrite < H2;reflexivity.
-qed.
-
-lemma in_list_tail : \forall l,x,y.in_list nat x (y::l) \to x \neq y \to in_list nat x l.
-intros;elim H;elim H2;generalize in match H3;elim a
- [simplify in H4;destruct H4;elim H1;reflexivity
- |simplify in H5;destruct H5;apply (ex_intro ? ? l1);apply (ex_intro ? ? a1);
- reflexivity]
-qed.
-
-lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
-intros;elim H;elim H1;generalize in match H2;generalize in match a;elim l 0
- [simplify;intro;elim l1
- [simplify in H3;destruct H3
- |simplify in H4;destruct H4]
- |intros;simplify in H4;apply (bool_elim ? (p t));intro
- [rewrite > H5 in H4;simplify in H4;generalize in match H4;elim l2
- [simplify in H6;destruct H6;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
- simplify;reflexivity
- |simplify in H7;destruct H7;apply in_list_cons;apply (H3 ? Hcut1);]
- |rewrite > H5 in H4;simplify in H4;apply in_list_cons;apply (H3 ? H4);]]
-qed.
-
-lemma in_list_filter_r : \forall l,p,x.in_list nat x l \to p x = true \to in_list nat x (filter nat l p).
-intros;elim H;elim H2;rewrite > H3;elim a
- [simplify;rewrite > H1;simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (filter nat a1 p));
- reflexivity
- |simplify;elim (p t);simplify
- [apply in_list_cons;assumption
- |assumption]]
-qed.
-
-lemma in_list_head : \forall x,l.in_list nat x (x::l).
-intros;apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity;
-qed.
-
-lemma 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;elim H;elim H1;clear H H1;generalize in match H2;elim a1
- [simplify in H;destruct H;left;reflexivity
- |simplify in H1;destruct H1;right;
- apply (ex_intro ? ? l1);
- apply (ex_intro ? ? a2);
- reflexivity]
-qed.
-
lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to
\exists p.p \leq m \land prime p \land p \divides n.
intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split
assumption]
qed.
-
-lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l.
-intros;elim l
- [simplify;apply le_n
- |simplify;apply (bool_elim ? (p t));intro
- [simplify;apply le_S_S;assumption
- |simplify;apply le_S;assumption]]
-qed.
-
-inductive sorted (P:nat \to nat \to Prop): list nat \to Prop \def
-| sort_nil : sorted P []
-| sort_cons : \forall x,l.sorted P l \to (\forall y.in_list ? y l \to P x y)
- \to sorted P (x::l).
-
-definition sorted_lt : list nat \to Prop \def \lambda l.sorted lt l.
-
-definition sorted_gt : list nat \to Prop \def \lambda l.sorted gt l.
-
-lemma sorted_cons_to_sorted : \forall P,x,l.sorted P (x::l) \to sorted P l.
-intros;inversion H;intros
- [destruct H1
- |destruct H4;assumption]
-qed.
-
-lemma sorted_to_minimum : \forall P,x,l.sorted P (x::l) \to
- \forall y.in_list ? y l \to P x y.
-intros;inversion H;intros;
- [destruct H2
- |destruct H5;apply H4;assumption]
-qed.
-
-lemma not_in_list_nil : \forall A,a.\lnot in_list A a [].
-intros;intro;elim H;elim H1;generalize in match H2;elim a1
- [simplify in H3;destruct H3
- |simplify in H4;destruct H4]
-qed.
+definition sorted_lt \def sorted ? lt.
+definition sorted_gt \def sorted ? gt.
lemma sieve_prime : \forall t,k,l2,l1.
(\forall p.(in_list ? p l1 \to prime p \land p \leq k \land \forall x.in_list ? x l2 \to p < x) \land
|apply (trans_le ? ? ? H11);
elim (in_list_cons_case ? ? ? ? H19)
[rewrite > H20;apply le_n
- |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);assumption]]]
+ |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]
|apply in_list_head]
|elim (H3 t1);elim H11
[elim H13;apply lt_to_le;assumption
|rewrite < H10;elim (H3 t1);elim H11
[elim H13;apply lt_to_le;assumption
|apply in_list_head]]
- |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);apply (in_list_filter ? ? ? H9)]]
+ |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]]
|elim (H2 p);elim (H9 H8);split
[assumption
|intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]]
|apply in_list_head]]]
|elim (in_list_cons_case ? ? ? ? H13)
[rewrite > H14;apply le_n
- |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);assumption]]]]
+ |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]]
|elim (H3 x);split;intros;
[split
[elim H7
[assumption
|intros;unfold;elim (H2 y);elim (H8 H7);
apply H11;apply in_list_head]
- |generalize in match (sorted_cons_to_sorted ? ? ? H6);elim l
+ |generalize in match (sorted_cons_to_sorted ? ? ? ? H6);elim l
[simplify;assumption
|simplify;elim (notb (divides_b t1 t2));simplify
- [lapply (sorted_cons_to_sorted ? ? ? H8);lapply (H7 Hletin);
- apply (sort_cons ? ? ? Hletin1);intros;
- apply (sorted_to_minimum ? ? ? H8);apply (in_list_filter ? ? ? H9);
- |apply H7;apply (sorted_cons_to_sorted ? ? ? H8)]]]]]
-qed.
-
-lemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
-intros;elim H;elim H1;generalize in match H2;elim a
- [simplify in H3;destruct H3;reflexivity
- |simplify in H4;destruct H4;generalize in match Hcut1;elim l
- [simplify in H4;destruct H4
- |simplify in H5;destruct H5]]
+ [lapply (sorted_cons_to_sorted ? ? ? ? H8);lapply (H7 Hletin);
+ apply (sort_cons ? ? ? ? Hletin1);intros;
+ apply (sorted_to_minimum ? ? ? ? H8);apply (in_list_filter ? ? ? H9);
+ |apply H7;apply (sorted_cons_to_sorted ? ? ? ? H8)]]]]]
qed.
lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to
k \leq n.
intros 2;elim m
[simplify in H;elim (not_in_list_nil ? ? H)
- |simplify in H1;elim H1;elim H2;generalize in match H3;elim a
- [simplify in H4;destruct H4;apply le_n
- |simplify in H5;destruct H5;apply lt_to_le;apply (H (S k));
- apply (ex_intro ? ? l);apply (ex_intro ? ? a1);assumption]]
+ |simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+ [rewrite > H2;apply le_n
+ |apply lt_to_le;apply H;assumption]]
qed.
lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n).
-intros;elim H
- [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? []);
- simplify;reflexivity
- |generalize in match H2;elim H1
- [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? [3]);simplify;reflexivity
- |simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (list_n_aux n2 3));
- simplify;reflexivity]]
+intros;elim H;simplify
+ [apply in_list_head
+ |generalize in match H2;elim H1;simplify;apply in_list_head]
qed.
lemma le_SSO_list_n : \forall m,n.in_list nat n (list_n m) \to 2 \leq n.
lemma le_list_n_aux : \forall n,m,k.in_list ? n (list_n_aux m k) \to n \leq k+m-1.
intros 2;elim m
[simplify in H;elim (not_in_list_nil ? ? H)
- |simplify in H1;elim H1;elim H2;generalize in match H3;elim a
- [simplify in H4;destruct H4;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O;
+ |simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+ [rewrite > H2;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O;
rewrite > plus_n_O in \vdash (? % ?);apply le_plus_r;apply le_O_n
- |simplify in H5;destruct H5;rewrite < plus_n_Sm;apply (H (S k));
- apply (ex_intro ? ? l);apply (ex_intro ? ? a1);assumption]]
+ |rewrite < plus_n_Sm;apply (H (S k));assumption]]
qed.
lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m.
intros;elim (decidable_le 2 n)
[elim (sieve_sound1 ? H);assumption
|generalize in match (le_S_S_to_le ? ? (not_le_to_lt ? ? H));cases n
- [intro;apply sort_nil
+ [intro;simplify;apply sort_nil
|intros;lapply (le_S_S_to_le ? ? H1);rewrite < (le_n_O_to_eq ? Hletin);
- apply sort_nil]]
+ simplify;apply sort_nil]]
qed.
lemma in_list_sieve_to_prime : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to
projects / helm.git / commitdiff