helm/software/matita/nlibrary/logic/cprop.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 include "hints_declaration.ma".
  16 include "sets/setoids1.ma".
  17
  18 ndefinition CPROP: setoid1.
  19  napply mk_setoid1
  20   [ napply CProp[0]
  21   | napply (mk_equivalence_relation1 CProp[0])
  22      [ napply iff
  23      | #x; napply mk_iff; #H; nassumption
  24      | #x; #y; *; #H1; #H2; napply mk_iff; nassumption
  25      | #x; #y; #z; *; #H1; #H2; *; #H3; #H4; napply mk_iff; #w
  26         [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
  27 nqed.
  28
  29 alias symbol "hint_decl" = "hint_decl_CProp2".
  30 unification hint 0 ≔ ⊢ CProp[0] ≡ carr1 CPROP.
  31
  32 (*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
  33 ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP
  34  on _x: carr1 CPROP to CProp[0].*)
  35
  36 alias symbol "eq" = "setoid1 eq".
  37
  38 ndefinition fi': ∀A,B:CPROP. A = B → B → A.
  39  #A; #B; #H; napply (fi … H); nassumption.
  40 nqed.
  41
  42 notation ". r" with precedence 50 for @{'fi $r}.
  43 interpretation "fi" 'fi r = (fi' ?? r).
  44
  45 ndefinition and_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
  46  napply (mk_binary_morphism1 … And);
  47  #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x; #y; @
  48   [ napply (. Ha^-1) | napply (. Hb^-1) | napply (. Ha) | napply (. Hb)] //.
  49 nqed.
  50
  51 unification hint 0 ≔ A,B:CProp[0];
  52   T ≟ CPROP,
  53   MM ≟ mk_unary_morphism1 ??
  54        (λX.mk_unary_morphism1 ?? (And X) (prop11 ?? (fun11 ?? and_morphism X)))
  55          (prop11 ?? and_morphism)
  56 (*-------------------------------------------------------------*) ⊢
  57   fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ And A B.
  58
  59 (*
  60 naxiom daemon: False.
  61
  62 nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
  63  #A; #A'; #B; #H1; #H2; napply (. (#‡H1)‡H2^-1); nelim daemon.
  64 nqed.
  65
  66 CSC: ugly proof term
  67 ncheck test.
  68 *)
  69
  70 ndefinition or_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
  71  napply (mk_binary_morphism1 … Or);
  72  #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x
  73   [ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //.
  74 nqed.
  75
  76 unification hint 0 ≔ A,B:CProp[0];
  77   T ≟ CPROP,
  78   MM ≟ mk_unary_morphism1 …
  79        (λX.mk_unary_morphism1 … (Or X) (prop11 … (fun11 ?? or_morphism X)))
  80          (prop11 … or_morphism)
  81 (*-------------------------------------------------------------*) ⊢
  82   fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ Or A B.
  83
  84 (* XXX always applied, generates hard unif problems
  85 ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
  86  napply (mk_binary_morphism1 … (λA,B:CProp[0]. A → B));
  87  #a; #a'; #b; #b'; #Ha; #Hb; @; #H; #x
  88   [ napply (. Hb^-1); napply H; napply (. Ha) | napply (. Hb); napply H; napply (. Ha^-1)]
  89  //.
  90 nqed.
  91
  92 unification hint 0 ≔ A,B:CProp[0];
  93   T ≟ CPROP,
  94   R ≟ mk_unary_morphism1 …
  95        (λX:CProp[0].mk_unary_morphism1 …
  96          (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
  97          (prop11 … if_morphism)
  98 (*----------------------------------------------------------------------*) ⊢
  99   fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R A) B ≡ A → B.
 100 *)
 101
 102 (* not as morphism *)
 103 nlemma Not_morphism : CProp[0] ⇒_1 CProp[0].
 104 @(λx:CProp[0].¬ x); #a b; *; #; @; /3/; nqed.
 105
 106 unification hint 0 ≔ P : CProp[0];
 107    A ≟ CPROP,
 108    B ≟ CPROP,
 109    M ≟ mk_unary_morphism1 ?? (λP.¬ P) (prop11 ?? Not_morphism)
 110 (*------------------------*)⊢
 111   fun11 A B M P ≡ ¬ P.
 112
 113 (* Ex setoid support *)
 114
 115 (* The caml, as some patches for it
 116 ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
 117 *)
 118
 119 (* simple case where the whole predicate can be rewritten *)
 120 nlemma Ex_morphism : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
 121 #S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P);
 122 #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
 123
 124 unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CPROP;
 125    A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
 126    B ≟ CPROP,
 127    M ≟ mk_unary_morphism1 ??
 128          (λP: (setoid1_of_setoid S) ⇒_1 CPROP.Ex (carr S) (fun11 ?? P))
 129          (prop11 ?? (Ex_morphism S))
 130 (*------------------------*)⊢
 131   fun11 A B M P ≡ Ex (carr S) (fun11 (setoid1_of_setoid S) CPROP P).
 132
 133 nlemma Ex_morphism_eta : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
 134 #S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S (λx.P x));
 135 #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
 136
 137 unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CPROP;
 138    A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
 139    B ≟ CPROP,
 140    M ≟ mk_unary_morphism1 ??
 141          (λP: (setoid1_of_setoid S) ⇒_1 CPROP.Ex (carr S) (λx.fun11 ?? P x))
 142          (prop11 ?? (Ex_morphism_eta S))
 143 (*------------------------*)⊢
 144   fun11 A B M P ≡ Ex (carr S) (λx.fun11 (setoid1_of_setoid S) CPROP P x).
 145
 146 nlemma Ex_setoid : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CPROP) → setoid.
 147 #T P; @ (Ex T (λx:T.P x)); @; ##[ #H1 H2; napply True |##*: //; ##] nqed.
 148
 149 unification hint 0 ≔ T : setoid,P ;
 150    S ≟ (Ex_setoid T P)
 151 (*---------------------------*) ⊢
 152    Ex (carr T) (λx:carr T.fun11 ?? P x) ≡ carr S.
 153
 154 (* couts how many Ex we are traversing *)
 155 ninductive counter : Type[0] ≝
 156  | End : counter
 157  | Next : (Prop → Prop) → (* dummy arg please the notation mechanism *)
 158           counter → counter.
 159
 160 (* to rewrite terms (live in setoid) *)
 161 nlet rec mk_P (S, T : setoid) (n : counter) on n ≝
 162   match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P S T m) ].
 163
 164 nlet rec mk_F (S, T : setoid) (n : counter) on n ≝
 165   match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F S T m) ].
 166
 167 nlet rec mk_E (S, T : setoid) (n : counter) on n : ∀f,g : mk_F S T n. CProp[0] ≝
 168   match n with
 169   [ End ⇒ λf,g:T. f = g
 170   | Next q m ⇒ λf,g: mk_F S T (Next q m). ∀x:S.mk_E S T m (f x) (g x) ].
 171
 172 nlet rec mk_H (S, T : setoid) (n : counter) on n :
 173 ∀P1,P2: mk_P S T n.∀f,g : mk_F S T n. CProp[1] ≝
 174   match n with
 175   [ End ⇒ λP1,P2:mk_P S T End.λf,g:T. f = g → P1 f =_1 P2 g
 176   | Next q m ⇒ λP1,P2: mk_P S T (Next q m).λf,g: mk_F S T (Next q m).
 177               ∀x:S.mk_H S T m (P1 x) (P2 x) (f x) (g x) ].
 178
 179 nlet rec mk_Ex (S, T : setoid) (n : counter) on n :
 180 ∀P: mk_P S T n.∀f : mk_F S T n. CProp[0] ≝
 181   match n with
 182   [ End ⇒ λP:mk_P S T End.λf:T. P f
 183   | Next q m ⇒ λP: mk_P S T (Next q m).λf: mk_F S T (Next q m).
 184               ∃x:S.mk_Ex S T m (P x) (f x) ].
 185
 186 nlemma Sig_generic : ∀S,T.∀n:counter.∀P,f,g.
 187   mk_E S T n f g → mk_H S T n P P f g → mk_Ex S T n P f =_1 mk_Ex S T n P g.
 188 #S T n; nelim n; nnormalize;
 189 ##[ #P f g E H; /2/;
 190 ##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
 191 nqed.
 192
 193 (* to rewrite propositions (live in setoid1) *)
 194 nlet rec mk_P1 (S : setoid) (T : setoid1) (n : counter) on n ≝
 195   match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P1 S T m) ].
 196
 197 nlet rec mk_F1 (S : setoid) (T : setoid1) (n : counter) on n ≝
 198   match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F1 S T m) ].
 199
 200 nlet rec mk_E1 (S : setoid) (T : setoid1) (n : counter) on n : ∀f,g : mk_F1 S T n. CProp[1] ≝
 201   match n with
 202   [ End ⇒ λf,g:T. f =_1 g
 203   | Next q m ⇒ λf,g: mk_F1 S T (Next q m). ∀x:S.mk_E1 S T m (f x) (g x) ].
 204
 205 nlet rec mk_H1 (S : setoid) (T : setoid1) (n : counter) on n :
 206 ∀P1,P2: mk_P1 S T n.∀f,g : mk_F1 S T n. CProp[1] ≝
 207   match n with
 208   [ End ⇒ λP1,P2:mk_P1 S T End.λf,g:T. f = g → P1 f =_1 P2 g
 209   | Next q m ⇒ λP1,P2: mk_P1 S T (Next q m).λf,g: mk_F1 S T (Next q m).
 210               ∀x:S.mk_H1 S T m (P1 x) (P2 x) (f x) (g x) ].
 211
 212 nlet rec mk_Ex1 (S : setoid) (T : setoid1) (n : counter) on n :
 213 ∀P: mk_P1 S T n.∀f : mk_F1 S T n. CProp[0] ≝
 214   match n with
 215   [ End ⇒ λP:mk_P1 S T End.λf:T. P f
 216   | Next q m ⇒ λP: mk_P1 S T (Next q m).λf: mk_F1 S T (Next q m).
 217               ∃x:S.mk_Ex1 S T m (P x) (f x) ].
 218
 219 nlemma Sig_generic1 : ∀S,T.∀n:counter.∀P,f,g.
 220   mk_E1 S T n f g → mk_H1 S T n P P f g → mk_Ex1 S T n P f =_1 mk_Ex1 S T n P g.
 221 #S T n; nelim n; nnormalize;
 222 ##[ #P f g E H; /2/;
 223 ##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
 224 nqed.
 225
 226 (* notation "∑x1,...,xn. E / H ; P" were:
 227    - x1...xn are bound in E and P, H is bound in P
 228    - H is an identifier that will have the type of E in P
 229    - P is the proof that the two existentially quantified predicates are equal*)
 230 notation > "∑ list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20
 231 for @{ 'Sig_gen
 232   ${ fold right @{ 'End }  rec acc @{ ('Next (λ${ident x}.${ident x}) $acc) } }
 233   ${ fold right @{ $E }              rec acc @{ λ${ident x}.$acc } }
 234   ${ fold right @{ λ${ident nE}.$H } rec acc @{ λ${ident x}.$acc } }
 235 }.
 236
 237 interpretation "next" 'Next x y = (Next x y).
 238 interpretation "end" 'End = End.
 239 interpretation "sig_gen" 'Sig_gen n E H = (Sig_generic  ?? n ??? E H).
 240 interpretation "sig_gen1" 'Sig_gen n E H = (Sig_generic1 ?? n ??? E H).
 241
 242 (*
 243 nlemma test0 : ∀S:setoid. ∀P: (setoid1_of_setoid S) ⇒_1 CPROP.∀f,g:S → S.
 244  (∀x:S.f x = g x) → (Ex S (λw.P (f w))) =_1 (Ex S (λw.P (g w))).
 245 #S P f g E; napply (∑w. E w / H ; ┼_1H); nqed.
 246
 247 nlemma test : ∀S:setoid. ∀P: (setoid1_of_setoid S) ⇒_1 CPROP.∀f,g:S → S.
 248  (∀x:S.f x = g x) → (Ex S (λw.P (f w)∧ True)) =_1 (Ex S (λw.P (g w)∧ True)).
 249 #S P f g E; napply (∑w. E w / H ; (┼_1H)╪_1#); nqed.
 250
 251 nlemma test_bound : ∀S:setoid. ∀e,f: (setoid1_of_setoid S) ⇒_1 CPROP. e = f →
 252    (Ex S (λw.e w ∧ True)) =_1 (Ex S (λw.f w ∧ True)).
 253 #S f g E; napply (.=_1 ∑x. E x x # / H ; (H ╪_1 #)); //; nqed.
 254
 255 nlemma test2 : ∀S:setoid. ∀ee: (setoid1_of_setoid S) ⇒_1 (setoid1_of_setoid S) ⇒_1 CPROP.
 256  ∀x,y:setoid1_of_setoid S.x =_1 y →
 257    (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
 258 #S m x y E; napply (.=_1 #╪_1(∑w. E / E ; ((E ╪_1 #) ╪_1 #))). //; nqed.
 259
 260 nlemma test3 : ∀S:setoid. ∀ee: (setoid1_of_setoid S) ⇒_1 (setoid1_of_setoid S) ⇒_1 CPROP.
 261  ∀x,y:setoid1_of_setoid S.x =_1 y →
 262    ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
 263 #S m x y E; napply (.=_1 (∑w. E / E ; ((E ╪_1 #) ╪_1 #)) ╪_1 #). //; nqed.
 264 *)
 265