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 ⊢
  52  mk_unary_morphism1 …
  53   (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
  54   (prop11 … and_morphism)
  55    A B ≡ And A B.
  56
  57 (*
  58 naxiom daemon: False.
  59
  60 nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
  61  #A; #A'; #B; #H1; #H2; napply (. (#‡H1)‡H2^-1); nelim daemon.
  62 nqed.
  63
  64 CSC: ugly proof term
  65 ncheck test.
  66 *)
  67
  68 ndefinition or_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
  69  napply (mk_binary_morphism1 … Or);
  70  #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x
  71   [ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //.
  72 nqed.
  73
  74 unification hint 0 ≔ A,B ⊢
  75  mk_unary_morphism1 …
  76   (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
  77   (prop11 … or_morphism)
  78   A B ≡ Or A B.
  79
  80 ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
  81  napply (mk_binary_morphism1 … (λA,B:CProp[0]. A → B));
  82  #a; #a'; #b; #b'; #Ha; #Hb; @; #H; #x
  83   [ napply (. Hb^-1); napply H; napply (. Ha) | napply (. Hb); napply H; napply (. Ha^-1)]
  84  //.
  85 nqed.
  86
  87 unification hint 0 ≔ A,B ⊢
  88  mk_unary_morphism1 …
  89   (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
  90   (prop11 … if_morphism)
  91   A B ≡ A → B.