weblib/basics/jmeq.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "basics/logic.ma".
  13
  14 \ 5img class="anchor" src="icons/tick.png" id="Sigma"\ 6inductive Sigma: Type[1] ≝
  15  mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
  16
  17 \ 5img class="anchor" src="icons/tick.png" id="p1"\ 6definition p1: \ 5a href="cic:/matita/basics/jmeq/Sigma.ind(1,0,0)"\ 6Sigma\ 5/a\ 6 → Type[0].
  18  #S cases S #Y #_ @Y
  19 qed.
  20
  21 \ 5img class="anchor" src="icons/tick.png" id="p2"\ 6definition p2: ∀S:\ 5a href="cic:/matita/basics/jmeq/Sigma.ind(1,0,0)"\ 6Sigma\ 5/a\ 6. \ 5a href="cic:/matita/basics/jmeq/p1.def(1)"\ 6p1\ 5/a\ 6 S.
  22  #S cases S #Y #x @x
  23 qed.
  24
  25 \ 5img class="anchor" src="icons/tick.png" id="jmeq"\ 6inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
  26 jmrefl : jmeq A x A x.
  27
  28 \ 5img class="anchor" src="icons/tick.png" id="eqProp"\ 6definition eqProp ≝ λA:Prop.\ 5a href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/a\ 6 A.
  29
  30 \ 5img class="anchor" src="icons/tick.png" id="K"\ 6lemma K : ∀A.∀x:A.∀h:x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x. \ 5a href="cic:/matita/basics/jmeq/eqProp.def(1)" title="null"\ 6eqProp\ 5/a\ 6 ? h (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 A x).
  31 #A #x #h @(\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? h: \ 5a href="cic:/matita/basics/jmeq/eqProp.def(1)"\ 6eqProp\ 5/a\ 6 ? ? ?).
  32 qed.
  33
  34 \ 5img class="anchor" src="icons/tick.png" id="cast"\ 6definition cast:
  35  ∀A,B:Type[0].∀E:A\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6B. A → B.
  36  #A #B #E cases E #X @X
  37 qed.
  38
  39 \ 5img class="anchor" src="icons/tick.png" id="tech1"\ 6lemma tech1:
  40  ∀Aa,Bb:\ 5a href="cic:/matita/basics/jmeq/Sigma.ind(1,0,0)"\ 6Sigma\ 5/a\ 6.∀E:Aa\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6Bb.
  41   \ 5a href="cic:/matita/basics/jmeq/cast.def(1)"\ 6cast\ 5/a\ 6 (\ 5a href="cic:/matita/basics/jmeq/p1.def(1)"\ 6p1\ 5/a\ 6 Aa) (\ 5a href="cic:/matita/basics/jmeq/p1.def(1)"\ 6p1\ 5/a\ 6 Bb) ? (\ 5a href="cic:/matita/basics/jmeq/p2.def(2)"\ 6p2\ 5/a\ 6 Aa) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/jmeq/p2.def(2)"\ 6p2\ 5/a\ 6 Bb.
  42  [2: >E %
  43  | #Aa #Bb #E >E cases Bb #B #b normalize % ]
  44 qed.
  45
  46 \ 5img class="anchor" src="icons/tick.png" id="gral"\ 6lemma gral: ∀A.∀x,y:A.
  47  \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A y → x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y.
  48  #A #x #y #E lapply (\ 5a href="cic:/matita/basics/jmeq/tech1.def(3)"\ 6tech1\ 5/a\ 6 ?? E)
  49  generalize in ⊢ (??(???%?)? → ?); #E1
  50  normalize in E1; >(\ 5a href="cic:/matita/basics/jmeq/K.def(2)"\ 6K\ 5/a\ 6 ?? E1) normalize
  51  #H @H
  52 qed.
  53
  54 \ 5img class="anchor" src="icons/tick.png" id="daemon"\ 6axiom daemon: \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
  55
  56 \ 5img class="anchor" src="icons/tick.png" id="jm_to_eq_sigma"\ 6lemma jm_to_eq_sigma:
  57  ∀A,x,y. \ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"\ 6jmeq\ 5/a\ 6 A x A y → \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A y.
  58  #A #x #y #E cases E in ⊢ (???%); %
  59 qed.
  60
  61 \ 5img class="anchor" src="icons/tick.png" id="curry"\ 6definition curry:
  62  ∀A,x.
  63   (∀y. \ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"\ 6jmeq\ 5/a\ 6 A x A y → Type[0]) →
  64    (∀y. \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A y → Type[0]).
  65  #A #x #f #y #E @(f y) >(\ 5a href="cic:/matita/basics/jmeq/gral.def(4)"\ 6gral\ 5/a\ 6 ??? E) %
  66 qed.
  67
  68 \ 5img class="anchor" src="icons/tick.png" id="G"\ 6lemma G : ∀A.∀x:A.∀P:∀y:A.\ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A y →Type[0].
  69  P x (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? (\ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A x)) → ∀y.∀h:\ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A y.
  70   P y h.
  71  #A #x #P #H #y #E lapply (\ 5a href="cic:/matita/basics/jmeq/gral.def(4)"\ 6gral\ 5/a\ 6 ??? E) #G generalize in match E;
  72  @(match G
  73     return λy.λ_. ∀e:\ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/jmeq/Sigma.con(0,1,0)"\ 6mk_Sigma\ 5/a\ 6 A y. P y e
  74    with
  75     [refl ⇒ ?])
  76  #E <(\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 ??? (\ 5a href="cic:/matita/basics/jmeq/K.def(2)"\ 6K\ 5/a\ 6 ?? E)) @H
  77 qed.
  78
  79 \ 5img class="anchor" src="icons/tick.png" id="PP"\ 6definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
  80  #A #P #a @(P a)
  81 qed.
  82
  83 \ 5img class="anchor" src="icons/tick.png" id="E"\ 6lemma E : ∀A.∀x:A.∀P:∀y:A.\ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"\ 6jmeq\ 5/a\ 6 A x A y→Type[0].
  84  \ 5a href="cic:/matita/basics/jmeq/PP.def(1)"\ 6PP\ 5/a\ 6 ? (P x) (\ 5a href="cic:/matita/basics/jmeq/jmeq.con(0,1,2)"\ 6jmrefl\ 5/a\ 6 A x) → ∀y.∀h:\ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"\ 6jmeq\ 5/a\ 6 A x A y.\ 5a href="cic:/matita/basics/jmeq/PP.def(1)"\ 6PP\ 5/a\ 6 ? (P y) h.
  85  #A #a #P #H #b #E letin F ≝ (\ 5a href="cic:/matita/basics/jmeq/jm_to_eq_sigma.def(1)"\ 6jm_to_eq_sigma\ 5/a\ 6 ??? E)
  86  lapply (\ 5a href="cic:/matita/basics/jmeq/G.def(5)"\ 6G\ 5/a\ 6 ?? (\ 5a href="cic:/matita/basics/jmeq/curry.def(5)"\ 6curry\ 5/a\ 6 ?? P) ?? F)
  87   [ normalize //
  88   | #H whd in H; @(H : \ 5a href="cic:/matita/basics/jmeq/PP.def(1)"\ 6PP\ 5/a\ 6 ? (P b) ?) ]
  89 qed.
  90
  91 \ 5img class="anchor" src="icons/tick.png" id="jmeq_elim"\ 6lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.\ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"\ 6jmeq\ 5/a\ 6 A x A y→Type[0].
  92  P x (\ 5a href="cic:/matita/basics/jmeq/jmeq.con(0,1,2)"\ 6jmrefl\ 5/a\ 6 A x) → ∀y.∀h:\ 5a href="cic:/matita/basics/jmeq/jmeq.ind(1,0,2)"\ 6jmeq\ 5/a\ 6 A x A y.P y h ≝ \ 5a href="cic:/matita/basics/jmeq/E.def(6)"\ 6E\ 5/a\ 6.