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 "sets/setoids1.ma".
  16
  17 ndefinition CPROP: setoid1.
  18  napply mk_setoid1
  19   [ napply CProp[0]
  20   | napply (mk_equivalence_relation1 CProp[0])
  21      [ napply iff
  22      | #x; napply mk_iff; #H; nassumption
  23      | #x; #y; *; #H1; #H2; napply mk_iff; nassumption
  24      | #x; #y; #z; *; #H1; #H2; *; #H3; #H4; napply mk_iff; #w
  25         [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
  26 nqed.
  27
  28 unification hint 0 ((λx,y.True) (carr1 CPROP) CProp[0]).
  29
  30 (*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
  31 ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP
  32  on _x: carr1 CPROP to CProp[0].*)
  33
  34 alias symbol "eq" = "setoid1 eq".
  35
  36 ndefinition fi': ∀A,B:CPROP. A = B → B → A.
  37  #A; #B; #H; napply (fi … H); nassumption.
  38 nqed.
  39
  40 notation ". r" with precedence 50 for @{'fi $r}.
  41 interpretation "fi" 'fi r = (fi' ?? r).
  42
  43 ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
  44  napply mk_binary_morphism1
  45   [ napply And
  46   | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #K1; #K2; napply conj
  47      [ napply (H1 K1)
  48      | napply (H3 K2)
  49      | napply (H2 K1)
  50      | napply (H4 K2)]##]
  51 nqed.
  52
  53 unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? and_morphism A B) (And A B)).
  54
  55 (*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
  56  #A; #A'; #B; #H1; #H2;
  57  napply (. ((#‡H1)‡H2^-1)); nnormalize;
  58 nqed.*)
  59
  60 (*interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).*)
  61
  62 ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
  63  napply mk_binary_morphism1
  64   [ napply Or
  65   | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #H;
  66      ##[##1,3: napply or_introl |##*: napply or_intror ]
  67    ##[ napply (H1 H)
  68      | napply (H2 H)
  69      | napply (H3 H)
  70      | napply (H4 H)]##]
  71 nqed.
  72
  73 unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? or_morphism A B) (Or A B)).
  74
  75 (*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*)
  76
  77 ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
  78  napply mk_binary_morphism1
  79   [ napply (λA,B. A → B)
  80   | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
  81      [ napply (if … H2); napply H; napply (fi … H1); nassumption
  82      | napply (fi … H2); napply H; napply (if … H1); nassumption]##]
  83 nqed.