1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/test/decl".
17 include "nat/times.ma".
18 include "nat/orders.ma".
20 inductive L (T:Type):Type:=
24 inductive eq (T:Type) : L T → L T → Prop :=
25 eq_refl:∀x:T. eq T (j ? x) (j ? x).
27 notation "hvbox(a break ≡ b)"
28 non associative with precedence 45
29 for @{ 'equiv $a $b }.
31 interpretation "uguaglianza parziale" 'equiv x y =
32 (cic:/matita/test/decl/eq.ind#xpointer(1/1) _ x y).
34 coercion cic:/matita/test/decl/L.ind#xpointer(1/1/2).
36 lemma sim: ∀T:Type. ∀x,y:T. (j ? x) ≡ (j ? y) → (j ? y) ≡ (j ? x).
43 lemma trans: ∀T:Type. ∀x,y,z:T.
44 (j ? x) ≡ (j ? y) → (j ? y) ≡ (j ? z) → (j ? x) ≡ (j ? z).
55 axiom Rplus: L R→L R→L R.
56 axiom Rmult: L R→L R→L R.(*
57 axiom Rdiv: L R→L R→L R.*)
59 axiom Relev: L R→L R→L R.
60 axiom Rle: L R→L R→Prop.
61 axiom Rge: L R→L R→Prop.
63 interpretation "real plus" 'plus x y =
64 (cic:/matita/test/decl/Rplus.con x y).
66 interpretation "real leq" 'leq x y =
67 (cic:/matita/test/decl/Rle.con x y).
69 interpretation "real geq" 'geq x y =
70 (cic:/matita/test/decl/Rge.con x y).
72 let rec elev (x:L R) (n:nat) on n: L R ≝
74 [O ⇒ match x with [bottom ⇒ bottom ? | j y ⇒ (j ? R1)]
75 | S n ⇒ Rmult x (elev x n)
78 let rec real_of_nat (n:nat) : L R ≝
81 | S n ⇒ real_of_nat n + (j ? R1)
84 coercion cic:/matita/test/decl/real_of_nat.con.
86 axiom Rplus_commutative: ∀x,y:R. (j ? x) + (j ? y) ≡ (j ? y) + (j ? x).
87 axiom R0_neutral: ∀x:R. (j ? x) + (j ? R0) ≡ (j ? x).
88 axiom Rmult_commutative: ∀x,y:R. Rmult (j ? x) (j ? y) ≡ Rmult (j ? y) (j ? x).
89 axiom R1_neutral: ∀x:R. Rmult (j ? x) (j ? R1) ≡ (j ? x).
92 ∀x:R. ¬((j ? x) ≡ (j ? R0)) → Rmult (Rinv (j ? x)) (j ? x) ≡ (j ? R1).
93 definition is_defined :=
94 λ T:Type. λ x:L T. ∃y:T. x = (j ? y).
95 axiom Rinv_ok2: ∀x:L R. ¬(x = bottom ?) → ¬(x ≡ (j ? R0)) → is_defined ? (Rinv x).
98 λ x,y:L R. Rmult x (Rinv y).
101 lemma pippo: ∀x:R. ¬((j ? x) ≡ (j ? R0)) → Rdiv (j ? R1) (j ? x) ≡ Rinv (j ? x).
104 elim (Rinv_ok2 ? ? H).
106 rewrite > Rmult_commutative.
110 axiom Rdiv_le: ∀x,y:R. (j ? R1) ≤ (j ? y) → Rdiv (j ? x) (j ? y) ≤ (j ? x).
111 axiom R2_1: (j ? R1) ≤ S (S O).
114 axiom Rdiv_pos: ∀ x,y:R.
115 (j ? R0) ≤ (j ? x) → (j ? R1) ≤ (j ? y) → (j ? R0) ≤ Rdiv (j ? x) (j ? y).
116 axiom Rle_R0_R1: (j ? R0) ≤ (j ? R1).
117 axiom div: ∀x:R. (j ? x) = Rdiv (j ? x) (S (S O)) → (j ? x) = O.