| T.Line line -> out_line_comment och line
| T.BaseUri uri -> out_command och (set "baseuri" uri)
| T.Include script -> out_command och (require script)
- | T.Coercion specs -> out_command och (coercion (snd specs))
+ | T.Coercion specs -> out_unexported och "COERCION" (snd specs)
| T.Notation specs -> out_unexported och "NOTATION" (snd specs) (**)
| T.Inline (_, T.Var, src, _) -> out_alias och (UriManager.name_of_uri (UriManager.uri_of_string src)) src
| T.Inline specs -> out_command och (inline (trd_rth specs))
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 12
+let magic = 13
type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
- | Coercion of loc * UriManager.uri * bool (* add_obj *) *
+ | Coercion of loc * 'term * bool (* add_obj *) *
int (* arity *) * int (* saturations *)
| Default of loc * string * UriManager.uri list
| Drop of loc
Printf.sprintf "default \"%s\" %s" what
(String.concat " " (List.map UriManager.string_of_uri uris))
-let pp_coercion uri do_composites arity saturations=
+let pp_coercion ~term_pp t do_composites arity saturations=
Printf.sprintf "coercion %s %d %d %s"
- (UriManager.string_of_uri uri) arity saturations
+ (term_pp t) arity saturations
(if do_composites then "" else "nocomposites")
let pp_command ~term_pp ~obj_pp = function
| Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
- | Coercion (_, uri, do_composites, i, j) ->
- pp_coercion uri do_composites i j
+ | Coercion (_, t, do_composites, i, j) ->
+ pp_coercion ~term_pp t do_composites i j
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
| Include (_,path) -> "include \"" ^ path ^ "\""
let uris = List.map rehash_uri uris in
GrafiteAst.Default (loc, name, uris)
| GrafiteAst.Coercion (loc, uri, close, arity, saturations) ->
- GrafiteAst.Coercion (loc, rehash_uri uri, close, arity, saturations)
+ GrafiteAst.Coercion (loc, CicUtil.rehash_term uri, close, arity, saturations)
| GrafiteAst.Index (loc, key, uri) ->
GrafiteAst.Index (loc, HExtlib.map_option CicUtil.rehash_term key, rehash_uri uri)
| cmd ->
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
let coercion_moo_statement_of (uri,arity, saturations) =
- GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity, saturations)
+ GrafiteAst.Coercion
+ (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
let refinement_toolkit = {
RefinementTool.type_of_aux' =
}
let eval_coercion status ~add_composites uri arity saturations =
+ let uri =
+ try CicUtil.uri_of_term uri
+ with Invalid_argument _ ->
+ raise (Invalid_argument "coercion can only be constants/constructors")
+ in
let status,compounds =
GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
saturations (GrafiteTypes.get_baseuri status)
in
let metasenv,key = disambiguate_term_option metasenv key in
!lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
- | GrafiteAst.Coercion _
+ | GrafiteAst.Coercion (loc,t,b,a,s) ->
+ let lexicon_status_ref = ref lexicon_status in
+ let disambiguate_term =
+ disambiguate_term text prefix_len lexicon_status_ref [] in
+ let metasenv,t = disambiguate_term metasenv t in
+ !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
| GrafiteAst.Default _
| GrafiteAst.Drop _
| GrafiteAst.Include _
ind_types
in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
- | IDENT "coercion" ; suri = URI ; arity = OPT int ;
- saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
+ | IDENT "coercion" ;
+ t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
+ arity = OPT int ; saturations = OPT int;
+ composites = OPT (IDENT "nocomposites") ->
let arity = match arity with None -> 0 | Some x -> x in
let saturations = match saturations with None -> 0 | Some x -> x in
let composites = match composites with None -> true | Some _ -> false in
GrafiteAst.Coercion
- (loc, UriManager.uri_of_string suri, composites, arity, saturations)
+ (loc, t, composites, arity, saturations)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
definition square_bishop_set : bishop_set → bishop_set.
intro S; apply (mk_bishop_set (S × S));
-[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
+[1: intros (x y); apply ((\fst x # \fst y) ∨ (\snd x # \snd y));
|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);
|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X);
|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
- [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
- |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
+ [1: cases (bs_cotransitive ??? (\fst z) X); [left;left|right;left]assumption;
+ |2: cases (bs_cotransitive ??? (\snd z) X); [left;right|right;right]assumption;]]
qed.
notation "s 2 \atop \neq" non associative with precedence 90
(**************************************************************************)
include "logic/equality.ma".
+include "datatypes/constructors.ma".
inductive Or (A,B:CProp) : CProp ≝
| Left : A → Or A B
interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t).
-coinductive product (A,B:Type) : Type ≝ pair : ∀a:A.∀b:B.product A B.
-
-notation "a \times b" left associative with precedence 70 for @{'product $a $b}.
-interpretation "prod" 'product a b = (product a b).
-
-definition first : ∀A.∀P.A × P → A ≝ λA,P,s.match s with [pair x _ ⇒ x].
-definition second : ∀A.∀P.A × P → P ≝ λA,P,s.match s with [pair _ y ⇒ y].
-
-interpretation "pair pi1" 'pi1 = (first _ _).
-interpretation "pair pi2" 'pi2 = (second _ _).
-interpretation "pair pi1" 'pi1a x = (first _ _ x).
-interpretation "pair pi2" 'pi2a x = (second _ _ x).
-interpretation "pair pi1" 'pi1b x y = (first _ _ x y).
-interpretation "pair pi2" 'pi2b x y = (second _ _ x y).
-
-notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
-with precedence 90 for @{ 'pair $a $b}.
-interpretation "pair" 'pair a b = (pair _ _ a b).
-
inductive exT (A:Type) (P:A→CProp) : CProp ≝
ex_introT: ∀w:A. P w → exT A P.
interpretation "CProp exists" 'exists \eta.x = (exT _ x).
interpretation "dependent pair" 'pair a b = (ex_introT _ _ a b).
-notation < "'fst' \nbsp x" non associative with precedence 90 for @{'pi1a $x}.
-notation < "'snd' \nbsp x" non associative with precedence 90 for @{'pi2a $x}.
-notation < "'fst' \nbsp x \nbsp y" non associative with precedence 90 for @{'pi1b $x $y}.
-notation < "'snd' \nbsp x \nbsp y" non associative with precedence 90 for @{'pi2b $x $y}.
-notation > "'fst'" non associative with precedence 90 for @{'pi1}.
-notation > "'snd'" non associative with precedence 90 for @{'pi2}.
-
definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
definition pi2exT ≝
λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p].
-interpretation "exT fst" 'pi1 = (pi1exT _ _).
-interpretation "exT fst" 'pi1a x = (pi1exT _ _ x).
-interpretation "exT fst" 'pi1b x y = (pi1exT _ _ x y).
-interpretation "exT snd" 'pi2 = (pi2exT _ _).
-interpretation "exT snd" 'pi2a x = (pi2exT _ _ x).
-interpretation "exT snd" 'pi2b x y = (pi2exT _ _ x y).
+interpretation "exT \fst" 'pi1 = (pi1exT _ _).
+interpretation "exT \fst" 'pi1a x = (pi1exT _ _ x).
+interpretation "exT \fst" 'pi1b x y = (pi1exT _ _ x y).
+interpretation "exT \snd" 'pi2 = (pi2exT _ _).
+interpretation "exT \snd" 'pi2a x = (pi2exT _ _ x).
+interpretation "exT \snd" 'pi2b x y = (pi2exT _ _ x y).
inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝
ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
definition pi2exT23 ≝
λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 _ x _ _ _ ⇒ x].
-interpretation "exT2 fst" 'pi1 = (pi1exT23 _ _ _ _).
-interpretation "exT2 snd" 'pi2 = (pi2exT23 _ _ _ _).
-interpretation "exT2 fst" 'pi1a x = (pi1exT23 _ _ _ _ x).
-interpretation "exT2 snd" 'pi2a x = (pi2exT23 _ _ _ _ x).
-interpretation "exT2 fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y).
-interpretation "exT2 snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y).
+interpretation "exT2 \fst" 'pi1 = (pi1exT23 _ _ _ _).
+interpretation "exT2 \snd" 'pi2 = (pi2exT23 _ _ _ _).
+interpretation "exT2 \fst" 'pi1a x = (pi1exT23 _ _ _ _ x).
+interpretation "exT2 \snd" 'pi2a x = (pi2exT23 _ _ _ _ x).
+interpretation "exT2 \fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y).
+interpretation "exT2 \snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y).
definition Not : CProp → Prop ≝ λx:CProp.x → False.
[1: intro j; cases (Hxy j); cases H3; cases H4; split;
[apply (H5 0);|apply (H7 0)]
|2: cases (H l u Xi 〈?,h〉) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
- cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
+ cases H4; split; [apply H5] intros (y Hy);cases (H6 (\fst y));[2:apply Hy];
exists [apply w] apply H7;
|3: cases (H l u Yi 〈?,h〉) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
- cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
+ cases H4; split; [apply H5] intros (y Hy);cases (H6 (\fst y));[2:apply Hy];
exists [apply w] apply H7;]]
qed.
alias symbol "pi2" = "pair pi2".
alias symbol "pi1" = "pair pi1".
alias symbol "and" = "logical and".
- apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n));
+ apply (∃_:unit.∀n:C square.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n));
|2: intros 4 (U H x Hx); simplify in Hx;
cases H (_ H1); cases (H1 x); apply H2; apply Hx;
|3: intros; cases H (_ PU); cases H1 (_ PV);
[1: exists [apply something] intro n; cases (PU n);
split; intros; try split;[apply H1;|apply H2] assumption;
|2: intros 2 (x Hx); cases Hx; cases H1; clear H1;
- cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5;
- cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8;
+ cases (PU 〈(\fst x),x1〉); lapply (H4 H2) as H5; simplify in H5;
+ cases (PU 〈x1,(\snd x)〉); lapply (H7 H3) as H8; simplify in H8;
generalize in match H5; generalize in match H8;
generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8;
cases x; simplify; intros; cases H1; clear H1; apply H4;
[constructor 1|constructor 2|constructor 3] assumption;
qed.
-alias symbol "pi1" = "exT fst".
+alias symbol "pi1" = "exT \fst".
alias symbol "leq" = "natural 'less or equal to'".
lemma nat_dedekind_sigma_complete:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
- ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
+ ∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉);
fold normalize X; intros; cases H1;
-letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = fst (a j)) ∨ (i < u ∧ s+i ≤ u + fst (a j))); (* s - aj <= max 0 (u - i) *)
+alias symbol "plus" = "natural plus".
+alias symbol "nat" = "Uniform space N".
+letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j))); (* s - aj <= max 0 (u - i) *)
letin m ≝ (hide ? (
let rec aux i ≝
match i with
| S m ⇒
let pred ≝ aux m in
let apred ≝ a pred in
- match cmp_nat (fst apred) s with
+ match cmp_nat (\fst apred) s with
[ cmp_eq _ ⇒ pred
| cmp_gt nP ⇒ match ? in False return λ_.nat with []
- | cmp_lt nP ⇒ fst (H3 apred nP)]]
+ | cmp_lt nP ⇒ \fst (H3 apred nP)]]
in aux
:
∀i:nat.∃j:nat.spec i j));unfold spec in aux ⊢ %;
rewrite > (?:s = O);
[2: cases Hs; lapply (os_le_to_nat_le ?? H1);
apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin).
- |1: intros; lapply (os_le_to_nat_le (fst (a O)) O (H2 O));
+ |1: intros; lapply (os_le_to_nat_le (\fst (a O)) O (H2 O));
lapply (le_n_O_to_eq ? Hletin); assumption;]
|2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n];
apply (trans_le ??? (os_le_to_nat_le ?? H1));
[1,3: left; split; [1,3: assumption |2: symmetry; assumption]
cut (u = S n1); [2: apply le_to_le_to_eq; assumption ]
clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
- cut (s = S (fst (a w)));
+ cut (s = S (\fst (a w)));
[2: apply le_to_le_to_eq; [2: assumption]
- change in H8 with (s + n1 ≤ S (n1 + fst (a w)));
+ change in H8 with (s + n1 ≤ S (n1 + \fst (a w)));
rewrite > plus_n_Sm in H8; rewrite > sym_plus in H8;
apply (le_plus_to_le ??? H8);]
cases (H3 (a w) H6);
- change with (s = fst (a w1));
- change in H4 with (fst (a w) < fst (a w1));
+ change with (s = \fst (a w1));
+ change in H4 with (\fst (a w) < \fst (a w1));
apply le_to_le_to_eq; [ rewrite > Hcut; assumption ]
- apply (os_le_to_nat_le (fst (a w1)) s (H2 w1));
+ apply (os_le_to_nat_le (\fst (a w1)) s (H2 w1));
|*: right; split; try assumption;
[1: rewrite > sym_plus in ⊢ (? ? %);
rewrite < H6; apply le_plus_r; assumption;
|2: cases (H3 (a w) H6);
- change with (s + S n1 ≤ u + fst (a w1));rewrite < plus_n_Sm;
+ change with (s + S n1 ≤ u + \fst (a w1));rewrite < plus_n_Sm;
apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
apply (le_plus ???? (le_n ?) H9);]]]]]
clearbody m; unfold spec in m; clear spec;
let rec find i u on u : nat ≝
match u with
[ O ⇒ (m i:nat)
- | S w ⇒ match eqb (fst (a (m i))) s with
+ | S w ⇒ match eqb (\fst (a (m i))) s with
[ true ⇒ (m i:nat)
| false ⇒ find (S i) w]]
in find
:
- ∀i,bound.∃j.i + bound = u → s = fst (a j));
-[1: cases (find (S n) n2); intro; change with (s = fst (a w));
+ ∀i,bound.∃j.i + bound = u → s = \fst (a j));
+[1: cases (find (S n) n2); intro; change with (s = \fst (a w));
apply H6; rewrite < H7; simplify; apply plus_n_Sm;
|2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
|3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
cases (m u); cases H4; clear H4; cases H5; clear H5; [assumption]
cases (not_le_Sn_n ? H4)]
clearbody find; cases (find O u);
-exists [apply w]; intros; change with (s = fst (a j));
+exists [apply w]; intros; change with (s = \fst (a j));
rewrite > (H4 ?); [2: reflexivity]
apply le_to_le_to_eq;
[1: apply os_le_to_nat_le;
rewrite < (H4 ?); [2: reflexivity] apply le_n;]
qed.
-alias symbol "pi1" = "exT fst".
+alias symbol "pi1" = "exT \fst".
alias symbol "leq" = "natural 'less or equal to'".
+alias symbol "nat" = "ordered set N".
axiom nat_dedekind_sigma_complete_r:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing →
- ∀x.x is_infimum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
+ ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
cases H (_); cases (H8 y); apply H9; cases (H8 p);
lapply (H12 H1) as H13; apply (le_le_eq);
[1: apply (le_transitive ???? H4); apply (Le≪ ? H13); assumption;
-|2: apply (le_transitive ????? H5); apply (Le≫ (snd p) H13); assumption;]
+|2: apply (le_transitive ????? H5); apply (Le≫ (\snd p) H13); assumption;]
qed.
interpretation "Ordered uniform space N" 'nat = nat_ordered_uniform_space.
interpretation "list nth" 'nth_appl l d i = (cic:/matita/list/list/nth.con _ l d i).
notation < "\rationals \sup 2" non associative with precedence 90 for @{'q2}.
-interpretation "Q x Q" 'q2 = (product Q Q).
+interpretation "Q x Q" 'q2 = (Prod Q Q).
let rec make_list (A:Type) (def:nat→A) (n:nat) on n ≝
match n with
with precedence 71 for @{'mk_list_appl $f $n}.
interpretation "'mk_list' appl" 'mk_list_appl f n = (make_list _ f n).
-alias symbol "pair" = "pair".
definition q0 : ℚ × ℚ ≝ 〈OQ,OQ〉.
notation < "0 \sub \rationals" with precedence 90 for @{'q0}.
interpretation "q0" 'q0 = q0.
notation < "[ \rationals \sup 2]" with precedence 90 for @{'lq2}.
-interpretation "lq2" 'lq2 = (list (product Q Q)).
+interpretation "lq2" 'lq2 = (list (Prod Q Q)).
notation < "[ \rationals \sup 2] \sup 2" with precedence 90 for @{'lq22}.
-interpretation "lq22" 'lq22 = (product (list (product Q Q)) (list (product Q Q))).
+interpretation "lq22" 'lq22 = (Prod (list (Prod Q Q)) (list (Prod Q Q))).
notation "'len'" with precedence 90 for @{'len}.
notation < "'len' \nbsp l" with precedence 70 for @{'len_appl $l}.
interpretation "len appl" 'len_appl l = (length _ l).
-alias symbol "pi1" = "exT fst".
definition eject ≝
λP.λp:∃x:(list (ℚ × ℚ)) × (list (ℚ × ℚ)).P x.match p with [ex_introT p _ ⇒ p].
coercion cic:/matita/dama/models/q_function/eject.con.
definition inject ≝
λP.λp:(list (ℚ × ℚ)) × (list (ℚ × ℚ)).λh:P p. ex_introT ? P p h.
+(*coercion inject with 0 1 nocomposites.*)
coercion cic:/matita/dama/models/q_function/inject.con 0 1 nocomposites.
+definition cb0h ≝ (λl.mk_list (λi.〈\fst (nth l q0 i),OQ〉) (length ? l)).
+
alias symbol "pi2" = "pair pi2".
alias symbol "pi1" = "pair pi1".
-alias symbol "pair" = "pair".
definition rebase:
q_f → q_f →
∃p:q_f × q_f.∀i.
- fst (nth (bars (fst p)) q0 i) =
- fst (nth (bars (snd p)) q0 i).
+ \fst (nth (bars (\fst p)) q0 i) =
+ \fst (nth (bars (\snd p)) q0 i).
intros (f1 f2); cases f1 (s1 l1); cases f2 (s2 l2); clear f1 f2;
-letin aux ≝ (
+letin spec ≝ (λl1,l2:list (ℚ × ℚ).λm:nat.λz:(list (ℚ × ℚ)) × (list (ℚ × ℚ)).True);
+letin aux ≝ (
let rec aux (l1,l2:list (ℚ × ℚ)) (n:nat) on n : (list (ℚ × ℚ)) × (list (ℚ × ℚ)) ≝
match n with
[ O ⇒ 〈[],[]〉
| S m ⇒
match l1 with
- [ nil ⇒
- let copy_l2_with_0 ≝ mk_list (λi.〈fst (nth l2 q0 i),OQ〉) (length ? l2) in
- 〈copy_l2_with_0, l2〉
- | cons he1 tl1 ⇒〈[],[]〉 (*
+ [ nil ⇒ 〈cb0h l2, l2〉
+ | cons he1 tl1 ⇒
match l2 with
- [ nil ⇒
- let copy_l1_with_0 ≝ mk_list (λi.〈fst (nth l1 q0 i),OQ〉) (length ? l1) in
- 〈l1, copy_l1_with_0〉
- | cons he2 tl2 ⇒
- let base1 ≝ fst he1 in
- let base2 ≝ fst he2 in
- let height1 ≝ snd he1 in
- let height2 ≝ snd he2 in
+ [ nil ⇒ 〈l1, cb0h l1〉
+ | cons he2 tl2 ⇒
+ let base1 ≝ (\fst he1) in
+ let base2 ≝ (\fst he2) in
+ let height1 ≝ (\snd he1) in
+ let height2 ≝ (\snd he2) in
match q_cmp base1 base2 with
[ q_eq _ ⇒
let rc ≝ aux tl1 tl2 m in
- 〈he1 :: fst rc,he2 :: snd rc〉
+ 〈he1 :: \fst rc,he2 :: \snd rc〉
| q_lt _ ⇒
let rest ≝ base2 - base1 in
let rc ≝ aux tl1 (〈rest,height2〉 :: tl2) m in
- 〈〈base1,height1〉 :: fst rc,〈base1,height2〉 :: snd rc〉
+ 〈〈base1,height1〉 :: \fst rc,〈base1,height2〉 :: \snd rc〉
| q_gt _ ⇒
let rest ≝ base1 - base2 in
let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in
- 〈〈base2,height1〉 :: fst rc,〈base2,height2〉 :: snd rc〉
-]]*)]]
-in aux : ∀l1,l2,m.∃p.True);
+ 〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉
+]]]]
+in aux); : ∀l1,l2,m.∃z.spec l1 l2 m z);
cases (q_cmp s1 s2);
[1: apply (mk_q_f s1);
lemma square_ordered_set: ordered_set → ordered_set.
intro O;
apply (mk_ordered_set (O × O));
-[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
+[1: intros (x y); apply (\fst x ≰ \fst y ∨ \snd x ≰ \snd y);
|2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
cases H (X X); apply (os_coreflexive ?? X);
|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2);
definition invert_os_relation ≝
λC:ordered_set.λU:C square → Prop.
- λx:C square. U 〈snd x,fst x〉.
+ λx:C square. U 〈\snd x,\fst x〉.
interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
lemma segment_square_of_ordered_set_square:
∀O:ordered_set.∀u,v:O.∀x:O square.
- fst x ∈ [u,v] → snd x ∈ [u,v] → {[u,v]} square.
-intros; split; exists; [1: apply (fst x) |3: apply (snd x)] assumption;
+ \fst x ∈ [u,v] → \snd x ∈ [u,v] → {[u,v]} square.
+intros; split; exists; [1: apply (\fst x) |3: apply (\snd x)] assumption;
qed.
coercion cic:/matita/dama/ordered_uniform/segment_square_of_ordered_set_square.con 0 2.
-alias symbol "pi1" (instance 4) = "exT fst".
-alias symbol "pi1" (instance 2) = "exT fst".
+alias symbol "pi1" (instance 4) = "exT \fst".
+alias symbol "pi1" (instance 2) = "exT \fst".
lemma ordered_set_square_of_segment_square :
∀O:ordered_set.∀u,v:O.{[u,v]} square → O square ≝
- λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
+ λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈\fst(\fst b),\fst(\snd b)〉.
coercion cic:/matita/dama/ordered_uniform/ordered_set_square_of_segment_square.con.
restriction_agreement ? l r U u →
restriction_agreement ? l r (inv U) (inv u).
intros 9; split; intro;
-[1: apply (unrestrict ????? (segment_square_of_ordered_set_square ??? 〈snd b,fst b〉 H2 H1) H H3);
-|2: apply (restrict ????? (segment_square_of_ordered_set_square ??? 〈snd b,fst b〉 H2 H1) H H3);]
+[1: apply (unrestrict ????? (segment_square_of_ordered_set_square ??? 〈\snd b,\fst b〉 H2 H1) H H3);
+|2: apply (restrict ????? (segment_square_of_ordered_set_square ??? 〈\snd b,\fst b〉 H2 H1) H H3);]
qed.
alias symbol "square" (instance 8) = "bishop set square".
lemma bs_of_ss:
∀O:ordered_set.∀u,v:O.{[u,v]} square → (bishop_set_of_ordered_set O) square ≝
- λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
+ λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈\fst(\fst b),\fst(\snd b)〉.
notation < "x \sub \neq" with precedence 91 for @{'bsss $x}.
interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
alias symbol "pair" (instance 2) = "dependent pair".
lemma ss_of_bs:
∀O:ordered_set.∀u,v:O.
- ∀b:O square.fst b ∈ [u,v] → snd b ∈ [u,v] → {[u,v]} square ≝
+ ∀b:O square.\fst b ∈ [u,v] → \snd b ∈ [u,v] → {[u,v]} square ≝
λO:ordered_set.λu,v:O.
- λb:(O:bishop_set) square.λH1,H2.〈〈fst b,H1〉,〈snd b,H2〉〉.
+ λb:(O:bishop_set) square.λH1,H2.〈〈\fst b,H1〉,〈\snd b,H2〉〉.
notation < "x \sub \nleq" with precedence 91 for @{'ssbs $x}.
interpretation "ss_of_bs" 'ssbs x = (ss_of_bs _ _ _ x _ _).
unfold segment_square_of_ordered_set_square;
cases b; intros; split; intro; assumption;
|2: intros 2 (x Hx); apply (restrict ?????? HuU); apply Hwu;
- cases Hx (m Hm); exists[apply (fst m)] apply Hm;]
+ cases Hx (m Hm); exists[apply (\fst m)] apply Hm;]
|4: intros (U HU x); cases HU (u Hu); cases Hu (Gu HuU); clear HU Hu;
cases (us_phi4 ?? Gu x) (Hul Hur);
split; intros;
(segment_ordered_uniform_space _ a b).
(* Lemma 3.2 *)
-alias symbol "pi1" = "exT fst".
+alias symbol "pi1" = "exT \fst".
lemma restric_uniform_convergence:
∀O:ordered_uniform_space.∀l,u:O.
∀x:{[l,u]}.
∀a:sequence {[l,u]}.
- ⌊n,fst (a n)⌋ uniform_converges (fst x) →
+ ⌊n,\fst (a n)⌋ uniform_converges (\fst x) →
a uniform_converges x.
intros 8; cases H1; cases H2; clear H2 H1;
cases (H ? H3) (m Hm); exists [apply m]; intros;
(b is_decreasing → b is_lower_located → b is_cauchy).
lemma segment_upperbound:
- ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound ⌊n,fst (a n)⌋.
-intros 5; change with (fst (a n) ≤ u); cases (a n); cases H; assumption;
+ ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound ⌊n,\fst (a n)⌋.
+intros 5; change with (\fst (a n) ≤ u); cases (a n); cases H; assumption;
qed.
lemma segment_lowerbound:
- ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound ⌊n,fst (a n)⌋.
-intros 5; change with (l ≤ fst (a n)); cases (a n); cases H; assumption;
+ ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound ⌊n,\fst (a n)⌋.
+intros 5; change with (l ≤ \fst (a n)); cases (a n); cases H; assumption;
qed.
lemma segment_preserves_uparrow:
∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h.
- ⌊n,fst (a n)⌋ ↑ x → a ↑ 〈x,h〉.
+ ⌊n,\fst (a n)⌋ ↑ x → a ↑ 〈x,h〉.
intros; cases H (Ha Hx); split [apply Ha] cases Hx;
split; [apply H1] intros;
-cases (H2 (fst y)); [2: apply H3;] exists [apply w] assumption;
+cases (H2 (\fst y)); [2: apply H3;] exists [apply w] assumption;
qed.
lemma segment_preserves_downarrow:
∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h.
- ⌊n,fst (a n)⌋ ↓ x → a ↓ 〈x,h〉.
+ ⌊n,\fst (a n)⌋ ↓ x → a ↓ 〈x,h〉.
intros; cases H (Ha Hx); split [apply Ha] cases Hx;
split; [apply H1] intros;
-cases (H2 (fst y));[2:apply H3]; exists [apply w] assumption;
+cases (H2 (\fst y));[2:apply H3]; exists [apply w] assumption;
qed.
(* Fact 2.18 *)
lemma segment_cauchy:
∀C:ordered_uniform_space.∀l,u:C.∀a:sequence {[l,u]}.
- a is_cauchy → ⌊n,fst (a n)⌋ is_cauchy.
+ a is_cauchy → ⌊n,\fst (a n)⌋ is_cauchy.
intros 7;
alias symbol "pi1" (instance 3) = "pair pi1".
alias symbol "pi2" = "pair pi2".
-apply (H (λx:{[l,u]} square.U 〈fst (fst x),fst (snd x)〉));
+apply (H (λx:{[l,u]} square.U 〈\fst (\fst x),\fst (\snd x)〉));
(unfold segment_ordered_uniform_space; simplify);
exists [apply U] split; [assumption;]
intro; cases b; intros; simplify; split; intros; assumption;
lemma restrict_uniform_convergence_uparrow:
∀C:ordered_uniform_space.property_sigma C →
∀l,u:C.exhaustive {[l,u]} →
- ∀a:sequence {[l,u]}.∀x:C. ⌊n,fst (a n)⌋ ↑ x →
+ ∀a:sequence {[l,u]}.∀x:C. ⌊n,\fst (a n)⌋ ↑ x →
x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges 〈x,h〉.
intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
[1: split;
lemma restrict_uniform_convergence_downarrow:
∀C:ordered_uniform_space.property_sigma C →
∀l,u:C.exhaustive {[l,u]} →
- ∀a:sequence {[l,u]}.∀x:C. ⌊n,fst (a n)⌋ ↓ x →
+ ∀a:sequence {[l,u]}.∀x:C. ⌊n,\fst (a n)⌋ ↓ x →
x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges 〈x,h〉.
intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
[1: split;
∀C:ordered_uniform_space.property_sigma C →
∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
-alias symbol "pair" = "pair".
+alias symbol "pair" = "Pair construction".
letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
match i with
lemma segment_ordered_set:
∀O:ordered_set.∀u,v:O.ordered_set.
intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
-[1: intros (x y); apply (fst x ≰ fst y);
+[1: intros (x y); apply (\fst x ≰ \fst y);
|2: intro x; cases x; simplify; apply os_coreflexive;
|3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]
qed.
(* Lemma 2.9 *)
lemma segment_preserves_supremum:
∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}.
- ⌊n,fst (a n)⌋ is_increasing ∧
- (fst x) is_supremum ⌊n,fst (a n)⌋ → a ↑ x.
+ ⌊n,\fst (a n)⌋ is_increasing ∧
+ (\fst x) is_supremum ⌊n,\fst (a n)⌋ → a ↑ x.
intros; split; cases H; clear H;
[1: apply H1;
|2: cases H2; split; clear H2;
[1: apply H;
- |2: clear H; intro y0; apply (H3 (fst y0));]]
+ |2: clear H; intro y0; apply (H3 (\fst y0));]]
qed.
lemma segment_preserves_infimum:
∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}.
- ⌊n,fst (a n)⌋ is_decreasing ∧
- (fst x) is_infimum ⌊n,fst (a n)⌋ → a ↓ x.
+ ⌊n,\fst (a n)⌋ is_decreasing ∧
+ (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
intros; split; cases H; clear H;
[1: apply H1;
|2: cases H2; split; clear H2;
[1: apply H;
- |2: clear H; intro y0; apply (H3 (fst y0));]]
+ |2: clear H; intro y0; apply (H3 (\fst y0));]]
qed.
(* Definition 2.10 *)
alias symbol "pi1" = "pair pi1".
definition square_segment ≝
λO:ordered_set.λa,b:O.λx:O square.
- And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x).
+ And4 (\fst x ≤ b) (a ≤ \fst x) (\snd x ≤ b) (a ≤ \snd x).
definition convex ≝
λO:ordered_set.λU:O square → Prop.
- ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y.
+ ∀p.U p → \fst p ≤ \snd p → ∀y. square_segment ? (\fst p) (\snd p) y → U y.
(* Definition 2.11 *)
definition upper_located ≝
(* Definition 2.13 *)
alias symbol "square" = "bishop set square".
-alias symbol "pair" = "pair".
+alias symbol "pair" = "Pair construction".
alias symbol "exists" = "exists".
alias symbol "and" = "logical and".
definition compose_bs_relations ≝
λC:bishop_set.λU,V:C square → Prop.
- λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
+ λx:C square.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
definition compose_os_relations ≝
λC:ordered_set.λU,V:C square → Prop.
- λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
+ λx:C square.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉.
interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b).
interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b).
definition invert_bs_relation ≝
λC:bishop_set.λU:C square → Prop.
- λx:C square. U 〈snd x,fst x〉.
+ λx:C square. U 〈\snd x,\fst x〉.
notation < "s \sup (-1)" with precedence 70 for @{ 'invert $s }.
notation < "s \sup (-1) x" with precedence 70
us_carr:> bishop_set;
us_unifbase: (us_carr square → Prop) → CProp;
us_phi1: ∀U:us_carr square → Prop. us_unifbase U →
- (λx:us_carr square.fst x ≈ snd x) ⊆ U;
+ (λx:us_carr square.\fst x ≈ \snd x) ⊆ U;
us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
us_phi3: ∀U:us_carr square → Prop. us_unifbase U →
@{\lambda ${ident i} : $ty. $p}
@{\lambda ${ident i} . $p}}}.
+notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
+with precedence 90 for @{ 'pair $a $b}.
+
+notation "hvbox(x break \times y)" with precedence 70
+for @{ 'product $x $y}.
+
+notation < "\fst \nbsp x" non associative with precedence 69 for @{'pi1a $x}.
+notation < "\snd \nbsp x" non associative with precedence 69 for @{'pi2a $x}.
+
+notation < "\fst \nbsp x \nbsp y" non associative with precedence 69 for @{'pi1b $x $y}.
+notation < "\snd \nbsp x \nbsp y" non associative with precedence 69 for @{'pi2b $x $y}.
+
+notation > "\fst" non associative with precedence 90 for @{'pi1}.
+notation > "\snd" non associative with precedence 90 for @{'pi2}.
+
notation "hvbox(a break \to b)"
right associative with precedence 20
for @{ \forall $_:$a.$b }.
</sect1>
<sect1 id="command_coercion">
<title>coercion</title>
- <para><userinput>coercion u</userinput></para>
+ <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
<para>
<variablelist>
<varlistentry>
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">coercion</emphasis> &uri;</para>
+ <para>
+ <emphasis role="bold">coercion</emphasis>
+ (&uri; | &term; <emphasis role="bold">with</emphasis>)
+ [ &nat; [&nat;]]
+ [ <emphasis role="bold">nocomposites</emphasis> ]
+ </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>Declares <command>u</command> as an implicit coercion
- from the type of its last argument (source)
- to its codomain (target). Every time a term <command>x</command>
+ <para>Declares <command>u</command> as an implicit coercion.
+ If the type of <command>u</command> is
+ <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
+ <command>T(n - ariety)</command> while its source is
+ <command>T(n - ariety - saturation - 1)</command>.
+ Every time a term <command>x</command>
of type source is used with expected type target, Matita
automatically replaces <command>x</command> with
- <command>(u ? … ? x)</command> to avoid a typing error.</para>
+ <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
+ Note that the number of <command>?</command> added after
+ <command>x</command> is saturation.
<para>Implicit coercions are not displayed to the user:
<command>(u ? … ? x)</command> is rendered simply
as <command>x</command>.</para>
and there is already a coercion <command>u'</command> of
target <command>s</command> or source <command>t</command>,
a composite implicit coercion is automatically computed
- by Matita.</para>
+ by Matita unless <emphasis role="bold">nocomposites</emphasis>
+ is specified.</para>
</listitem>
</varlistentry>
</variablelist>
].
*)
+alias id "numeratorQ" = "cic:/matita/Q/q/q/numeratorQ.con".
+alias id "nat" = "cic:/matita/nat/nat/nat.ind#xpointer(1/1)".
+alias id "defactorize" = "cic:/matita/nat/factorization/defactorize.con".
+alias id "Q" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1)".
definition numQ:Q \to nat \def
\lambda q. defactorize (numeratorQ q).
+alias id "Qinv" = "cic:/matita/Q/q/qinv/Qinv.con".
definition denomQ:Q \to nat \def
\lambda q. defactorize (numeratorQ (Qinv q)).
]
qed.*)
+alias id "Qpos" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/2)".
+alias id "OQ" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/1)".
definition Qabs:Q \to Q \def \lambda q.
match q with
[OQ \Rightarrow OQ
include "Q/q.ma".
+alias id "finv" = "cic:/matita/Q/fraction/finv/finv.con".
theorem denominator_integral_factor_finv:
∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
intro;
elim z; simplify; reflexivity]
qed.
+alias id "Qpos" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/2)".
definition is_positive ≝
λq.
match q with
| _ ⇒ False
].
+alias id "Qneg" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/3)".
definition is_negative ≝
λq.
match q with
| _ ⇒ False
].
+(*
theorem is_positive_denominator_Qinv:
∀q. is_positive q → enumerator q = denominator (Qinv q).
intro;
assumption
| elim q in H ⊢ %; assumption]
qed.
+*)
\ No newline at end of file
include "Z/plus.ma".
include "nat/factorization.ma".
+alias id "pp" = "cic:/matita/Q/fraction/fraction/fraction.ind#xpointer(1/1/1)".
+alias id "cons" = "cic:/matita/Q/fraction/fraction/fraction.ind#xpointer(1/1/3)".
let rec enumerator_integral_fraction l ≝
match l with
[ pp n ⇒ Some ? l
]
].
+(*
definition enumerator_of_fraction ≝
λq.
match q with
| Qpos r ⇒ denominator_of_fraction r
| Qneg r ⇒ denominator_of_fraction r
].
+*)
\ No newline at end of file
[ O \Rightarrow OZ
| (S n)\Rightarrow pos n].
-coercion cic:/matita/Z/z/Z_of_nat.con.
+coercion Z_of_nat.
definition neg_Z_of_nat \def
\lambda n. match n with
interpretation "Pair construction" 'pair x y =
(cic:/matita/datatypes/constructors/Prod.ind#xpointer(1/1/1) _ _ x y).
-notation "hvbox(\langle x break , y \rangle )" with precedence 89
-for @{ 'pair $x $y}.
-
interpretation "Product" 'product x y =
(cic:/matita/datatypes/constructors/Prod.ind#xpointer(1/1) x y).
-notation "hvbox(x break \times y)" with precedence 89
-for @{ 'product $x $y}.
-
definition fst \def \lambda A,B:Type.\lambda p: Prod A B.
match p with
[(pair a b) \Rightarrow a].
match p with
[(pair a b) \Rightarrow b].
-interpretation "First projection" 'fst x =
- (cic:/matita/datatypes/constructors/fst.con _ _ x).
-
-notation "\fst x" with precedence 89
-for @{ 'fst $x}.
-
-interpretation "Second projection" 'snd x =
- (cic:/matita/datatypes/constructors/snd.con _ _ x).
-
-notation "\snd x" with precedence 89
-for @{ 'snd $x}.
+interpretation "pair pi1" 'pi1 = (fst _ _).
+interpretation "pair pi2" 'pi2 = (snd _ _).
+interpretation "pair pi1" 'pi1a x = (fst _ _ x).
+interpretation "pair pi2" 'pi2a x = (snd _ _ x).
+interpretation "pair pi1" 'pi1b x y = (fst _ _ x y).
+interpretation "pair pi2" 'pi2b x y = (snd _ _ x y).
theorem eq_pair_fst_snd: \forall A,B:Type.\forall p:Prod A B.
-p = 〈 (\fst p), (\snd p) 〉.
+p = 〈 \fst p, \snd p 〉.
intros.elim p.simplify.reflexivity.
qed.
(* XXX le coercion nel cast non vengono inserite *)
definition nat_canonical_eqType : nat → nat_eqType :=
λn : nat.(n : sort nat_eqType).
-coercion cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con.
+coercion nat_canonical_eqType.
definition bcmp ≝ λx,y:bool. match x with [ true ⇒ y | false => notb y ].
definition bool_eqType : eqType ≝ mk_eqType ? ? bcmpP.
definition bool_canonical_eqType : bool → bool_eqType :=
λb : bool.(b : sort bool_eqType).
-coercion cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con.
+coercion bool_canonical_eqType.
(* ### subtype of an eqType ### *)
definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d).
definition option_canonical_eqType : ∀d:eqType.d → option_eqType d ≝
λd:eqType.λx:d.(Some ? x : sort (option_eqType d)).
-coercion cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con.
+coercion option_canonical_eqType.
(* belle le coercions! *)
definition test_canonical_option_eqType ≝
]
].
-coercion cic:/matita/demo/power_derivative/inj.con.
+coercion inj.
axiom Rplus_Rzero_x: ∀x:R.0+x=x.
axiom Rplus_comm: symmetric ? Rplus.
definition costante : nat → R → R ≝
λa:nat.λx:R.inj a.
-coercion cic:/matita/demo/power_derivative/costante.con 1.
+coercion costante with 1.
axiom f_eq_extensional:
∀f,g:R→R.(∀x:R.f x = g x) → f=g.
qed.
(* *)
-coercion cic:/matita/logic/equality/sym_eq.con.
-coercion cic:/matita/logic/equality/eq_f.con.
+coercion sym_eq.
+coercion eq_f.
(* *)
default "equality"
projects / helm.git / commitdiff