source: src/ASM/JMCoercions.ma @ 1280

Last change on this file since 1280 was 1062, checked in by mulligan, 10 years ago

separated jmeq and coercions from foldstuff.ma in order to fix the ongoing mess in util.ma surrounding reduce_strong

File size: 1.4 KB
Line 
1include "basics/jmeq.ma".
2include "basics/types.ma".
3include "basics/list.ma".
4
5notation > "hvbox(a break ≃ b)"
6  non associative with precedence 45
7for @{ 'jmeq ? $a ? $b }.
8
9notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
10  non associative with precedence 45
11for @{ 'jmeq $t $a $u $b }.
12
13interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
14
15lemma eq_to_jmeq:
16  ∀A: Type[0].
17  ∀x, y: A.
18    x = y → x ≃ y.
19  //
20qed.
21
22definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
23definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
24
25coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
26coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
27
28(*axiom VOID: Type[0].
29axiom assert_false: VOID.
30definition bigbang: ∀A:Type[0].False → VOID → A.
31 #A #abs cases abs
32qed.
33
34coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.*)
35
36lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
37 #A #P #p cases p #w #q @q
38qed.
39
40lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
41 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
42qed.
43
44coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
45
46(* END RUSSELL **)
Note: See TracBrowser for help on using the repository browser.