helm/software/matita/contribs/igft/igft.ma

   1
   2 record powerset (A : Type) : Type := { content : A → CProp }.
   3
   4 notation > "Ω ^ A" non associative with precedence 50 for @{'P $A}.
   5 notation "Ω \sup A" non associative with precedence 50 for @{'P $A}.
   6 interpretation "Powerset" 'P A = (powerset A).
   7
   8 record AxiomSet : Type := {
   9   S :> Type;
  10   I_ : S → Type;
  11   C_ : ∀a.I_ a → Ω ^ S
  12 }.
  13
  14 notation > "∀ident a∈A.P" right associative with precedence 20
  15 for @{ ∀${ident a} : S $A. $P }.
  16 notation > "λident a∈A.P" right associative with precedence 20
  17 for @{ λ${ident a} : S $A. $P }.
  18
  19 notation "'I'" non associative with precedence 90 for @{'I}.
  20 interpretation "I" 'I = (I_ _).
  21 notation < "'I' \lpar a \rpar" non associative with precedence 90 for @{'I1 $a}.
  22 interpretation "I a" 'I1 a = (I_ _ a).
  23 notation "'C'" non associative with precedence 90 for @{'C}.
  24 interpretation "C" 'C = (C_ _).
  25 notation < "'C' \lpar a \rpar" non associative with precedence 90 for @{'C1 $a}.
  26 interpretation "C a" 'C1 a = (C_ _ a).
  27 notation < "'C' \lpar a , i \rpar" non associative with precedence 90 for @{'C2 $a $i}.
  28 interpretation "C a i" 'C2 a i = (C_ _ a i).
  29
  30 definition in_subset :=
  31   λA:AxiomSet.λa∈A.λU:Ω^A.content A U a.
  32
  33 notation "hvbox(a break εU)" non associative with precedence 50 for
  34 @{'in_subset $a $U}.
  35 interpretation "In subset" 'in_subset a U = (in_subset _ a U).
  36
  37 definition for_all ≝ λA:AxiomSet.λU:Ω^A.λP:A → CProp.∀x.xεU → P x.
  38
  39 inductive covers (A : AxiomSet) (U : Ω ^ A) : A → CProp :=
  40  | refl_ : ∀a.aεU → covers A U a
  41  | infinity_ : ∀a.∀i : I a. for_all A (C a i) (covers A U)  → covers A U a.
  42
  43 notation "'refl'" non associative with precedence 90 for @{'refl}.
  44 interpretation "refl" 'refl = (refl_ _ _ _).
  45
  46 notation "'infinity'" non associative with precedence 90 for @{'infinity}.
  47 interpretation "infinity" 'infinity = (infinity_ _ _ _).
  48
  49 notation "U ⊲ V" non associative with precedence 45
  50 for @{ 'covers_subsets $U $V}.
  51 interpretation "Covers subsets" 'covers_subsets U V = (for_all _ U (covers _ V)).
  52 interpretation "Covers elem subset" 'covers_subsets U V = (covers _ V U).
  53
  54 definition subseteq := λA:AxiomSet.λU,V:Ω^A.∀x.xεU → xεV.
  55
  56 interpretation "subseteq" 'subseteq u v = (subseteq _ u v).
  57
  58
  59 definition covers_elim_ ≝
  60  λA:AxiomSet.λU,P: Ω^A.λH1: U ⊆ P.
  61   λH2:∀a∈A.∀j:I a. C a j ⊲ U → C a j ⊆ P → aεP.
  62     let rec aux (a:A) (p:a ⊲ U) on p : aεP ≝
  63      match p return λr.λ_:r ⊲ U.r ε P with
  64       [ refl_ a q ⇒ H1 a q
  65       | infinity_ a j q ⇒ H2 a j q (λb.λr. aux b (q b r))]
  66     in
  67      aux.
  68
  69 interpretation "char" 'subset p = (mk_powerset _ p).
  70
  71 definition covers_elim :
  72  ∀A:AxiomSet.∀U: Ω^A.∀P:A→CProp.∀H1: U ⊆ {x | P x}.
  73   ∀H2:∀a∈A.∀j:I a. C a j ⊲ U → C a j ⊆ {x | P x} → P a.
  74    ∀a∈A.a ⊲ U → P a.
  75 change in ⊢ (?→?→?→?→?→?→?→%) with (aε{x|P x});
  76 intros 3; apply covers_elim_;
  77 qed.
  78
  79 theorem trans_: ∀A:AxiomSet.∀a∈A.∀U,V. a ⊲ U → U ⊲ V → a ⊲ V.
  80  intros;
  81  elim H using covers_elim;
  82   [ intros 2; apply (H1 ? H2);
  83   | intros; apply (infinity j);
  84     intros 2; apply (H3 ? H4);]
  85 qed.
  86
  87 notation "'trans'" non associative with precedence 90 for @{'trans}.
  88 interpretation "trans" 'trans = (trans_ _ _).
  89