matita/contribs/dama/dama_didactic/bottom.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "nat/times.ma".
  18 include "nat/orders.ma".
  19
  20 include "decl.ma".
  21
  22 inductive L (T:Type):Type:=
  23   bottom: L T
  24  |j: T → L T.
  25
  26 inductive eq (T:Type) : L T → L T → Prop :=
  27  eq_refl:∀x:T. eq T (j ? x) (j ? x).
  28
  29 notation "hvbox(a break ≡ b)"
  30   non associative with precedence 45
  31 for @{ 'equiv $a $b }.
  32
  33 interpretation "uguaglianza parziale" 'equiv x y =
  34  (cic:/matita/tests/decl/eq.ind#xpointer(1/1) _ x y).
  35
  36 coercion cic:/matita/tests/decl/L.ind#xpointer(1/1/2).
  37
  38 lemma sim: ∀T:Type. ∀x,y:T. (j ? x) ≡ (j ? y) → (j ? y) ≡ (j ? x).
  39  intros.
  40  inversion H.
  41  intros.
  42  apply eq_refl.
  43 qed.
  44
  45 lemma trans: ∀T:Type. ∀x,y,z:T.
  46  (j ? x) ≡ (j ? y) → (j ? y) ≡ (j ? z) → (j ? x) ≡ (j ? z).
  47  intros.
  48  inversion H1.
  49  intros.
  50  rewrite > H2 in H.
  51  assumption.
  52 qed.
  53
  54 axiom R:Type.
  55 axiom R0:R.
  56 axiom R1:R.
  57 axiom Rplus: L R→L R→L R.
  58 axiom Rmult: L R→L R→L R.(*
  59 axiom Rdiv: L R→L R→L R.*)
  60 axiom Rinv: L R→L R.
  61 axiom Relev: L R→L R→L R.
  62 axiom Rle: L R→L R→Prop.
  63 axiom Rge: L R→L R→Prop.
  64
  65 interpretation "real plus" 'plus x y =
  66  (cic:/matita/tests/decl/Rplus.con x y).
  67
  68 interpretation "real leq" 'leq x y =
  69  (cic:/matita/tests/decl/Rle.con x y).
  70
  71 interpretation "real geq" 'geq x y =
  72  (cic:/matita/tests/decl/Rge.con x y).
  73
  74 let rec elev (x:L R) (n:nat) on n: L R ≝
  75  match n with
  76   [O ⇒ match x with [bottom ⇒ bottom ? | j y ⇒ (j ? R1)]
  77   | S n ⇒ Rmult x (elev x n)
  78   ].
  79
  80 let rec real_of_nat (n:nat) : L R ≝
  81  match n with
  82   [ O ⇒ (j ? R0)
  83   | S n ⇒ real_of_nat n + (j ? R1)
  84   ].
  85
  86 coercion cic:/matita/tests/decl/real_of_nat.con.
  87
  88 axiom Rplus_commutative: ∀x,y:R. (j ? x) + (j ? y) ≡ (j ? y) + (j ? x).
  89 axiom R0_neutral: ∀x:R. (j ? x) + (j ? R0) ≡ (j ? x).
  90 axiom Rmult_commutative: ∀x,y:R. Rmult (j ? x) (j ? y) ≡ Rmult (j ? y) (j ? x).
  91 axiom R1_neutral: ∀x:R. Rmult (j ? x) (j ? R1) ≡ (j ? x).
  92
  93 axiom Rinv_ok:
  94  ∀x:R. ¬((j ? x) ≡ (j ? R0)) → Rmult (Rinv (j ? x)) (j ? x) ≡ (j ? R1).
  95 definition is_defined :=
  96  λ T:Type. λ x:L T. ∃y:T. x = (j ? y).
  97 axiom Rinv_ok2: ∀x:L R. ¬(x = bottom ?) → ¬(x ≡ (j ? R0)) → is_defined ? (Rinv x).
  98
  99 definition Rdiv :=
 100  λ x,y:L R. Rmult x (Rinv y).
 101
 102 (*
 103 lemma pippo: ∀x:R. ¬((j ? x) ≡ (j ? R0)) → Rdiv (j ? R1) (j ? x) ≡ Rinv (j ? x).
 104  intros.
 105  unfold Rdiv.
 106  elim (Rinv_ok2 ? ? H).
 107  rewrite > H1.
 108  rewrite > Rmult_commutative.
 109  apply R1_neutral.
 110 *)
 111
 112 axiom Rdiv_le: ∀x,y:R. (j ? R1) ≤ (j ? y) → Rdiv (j ? x) (j ? y) ≤ (j ? x).
 113 axiom R2_1: (j ? R1) ≤ S (S O).
 114
 115
 116 axiom Rdiv_pos: ∀ x,y:R.
 117  (j ? R0) ≤ (j ? x) → (j ? R1) ≤ (j ? y) → (j ? R0) ≤ Rdiv (j ? x) (j ? y).
 118 axiom Rle_R0_R1: (j ? R0) ≤ (j ? R1).
 119 axiom div: ∀x:R. (j ? x) = Rdiv (j ? x) (S (S O)) → (j ? x) = O.