refactor(library/logic): cleanup some of the proofs in cast.lean, remove piext axiom
Remark: the main motivation for piext was Lean 0.1 simplifier. We are using a different approach in Lean 0.2. The axiom is not needed anymore. It is also not used in any part of the standard library
This commit is contained in:
Leonardo de Moura
parent
09b533a965
commit
d306c42a1f
5 changed files with 44 additions and 86 deletions
|
|
@ -6,6 +6,5 @@ Axioms that extend the Calculus of Constructions.
|
|||
* [funext](funext.lean) : function extensionality
|
||||
* [classical](classical.lean) : the law of the excluded middle
|
||||
* [hilbert](hilbert.lean) : choice functions
|
||||
* [piext](piext.lean) : equality of Pi types
|
||||
* [prop_decidable](prop_decidable.lean) : the decidable class is trivial with excluded middle
|
||||
* [examples](examples/examples.md)
|
||||
|
|
@ -4,5 +4,5 @@
|
|||
--- Author: Jeremy Avigad
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
import logic.axioms.classical logic.axioms.funext logic.axioms.hilbert logic.axioms.piext
|
||||
import logic.axioms.prop_decidable
|
||||
import logic.axioms.classical logic.axioms.funext logic.axioms.hilbert
|
||||
import logic.axioms.prop_decidable
|
||||
|
|
|
|||
|
|
@ -29,6 +29,6 @@ namespace function
|
|||
theorem hfunext {A : Type} {B : A → Type} {B' : A → Type} {f : Π x, B x} {g : Π x, B' x}
|
||||
(H : ∀ a, f a == g a) : f == g :=
|
||||
let HH : B = B' := (funext (λ x, heq.type_eq (H x))) in
|
||||
cast_to_heq (funext (λ a, heq.to_eq (heq.trans (cast_app' HH f a) (H a))))
|
||||
cast_to_heq (funext (λ a, heq.to_eq (heq.trans (cast_app HH f a) (H a))))
|
||||
|
||||
end function
|
||||
|
|
|
|||
|
|
@ -1,33 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
|
||||
import logic.inhabited logic.cast
|
||||
|
||||
open inhabited
|
||||
|
||||
-- Pi extensionality
|
||||
axiom piext {A : Type} {B B' : A → Type} [H : inhabited (Π x, B x)] :
|
||||
(Π x, B x) = (Π x, B' x) → B = B'
|
||||
|
||||
-- TODO: generalize to eq_rec
|
||||
theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x)
|
||||
(a : A) : cast H f a == f a :=
|
||||
have Hi [visible] : inhabited (Π x, B x), from inhabited.mk f,
|
||||
have Hb : B = B', from piext H,
|
||||
cast_app' Hb f a
|
||||
|
||||
theorem hcongr_fun {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
|
||||
(H : f == f') : f a == f' a :=
|
||||
have Hi [visible] : inhabited (Π x, B x), from inhabited.mk f,
|
||||
have Hb : B = B', from piext (heq.type_eq H),
|
||||
hcongr_fun' a H Hb
|
||||
|
||||
theorem hcongr {A A' : Type} {B : A → Type} {B' : A' → Type}
|
||||
{f : Π x, B x} {f' : Π x, B' x} {a : A} {a' : A'}
|
||||
(Hff' : f == f') (Haa' : a == a') : f a == f' a' :=
|
||||
have H1 : ∀ (B B' : A → Type) (f : Π x, B x) (f' : Π x, B' x), f == f' → f a == f' a, from
|
||||
take B B' f f' e, hcongr_fun a e,
|
||||
have H2 : ∀ (B : A → Type) (B' : A' → Type) (f : Π x, B x) (f' : Π x, B' x),
|
||||
f == f' → f a == f' a', from heq.subst Haa' H1,
|
||||
H2 B B' f f' Hff'
|
||||
|
|
@ -58,7 +58,7 @@ namespace heq
|
|||
drec_on H !cast_eq
|
||||
|
||||
theorem to_eq (H : a == a') : a = a' :=
|
||||
calc
|
||||
calc
|
||||
a = cast (eq.refl A) a : cast_eq
|
||||
... = a' : to_cast_eq H
|
||||
|
||||
|
|
@ -81,7 +81,7 @@ section
|
|||
|
||||
-- should H₁ be explicit (useful in e.g. hproof_irrel)
|
||||
theorem eq_rec_to_heq {H₁ : a = a'} {p : P a} {p' : P a'} (H₂ : eq.rec_on H₁ p = p') : p == p' :=
|
||||
calc
|
||||
calc
|
||||
p == eq.rec_on H₁ p : heq.symm (eq_rec_heq H₁ p)
|
||||
... = p' : H₂
|
||||
|
||||
|
|
@ -95,9 +95,9 @@ section
|
|||
eq_true_elim (heq.to_eq H)
|
||||
|
||||
--TODO: generalize to eq.rec. This is a special case of rec_on_compose in eq.lean
|
||||
theorem cast_trans (Hab : A = B) (Hbc : B = C) (a : A) :
|
||||
theorem cast_trans (Hab : A = B) (Hbc : B = C) (a : A) :
|
||||
cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
|
||||
heq.to_eq (calc
|
||||
heq.to_eq (calc
|
||||
cast Hbc (cast Hab a) == cast Hab a : eq_rec_heq Hbc (cast Hab a)
|
||||
... == a : eq_rec_heq Hab a
|
||||
... == cast (Hab ⬝ Hbc) a : heq.symm (eq_rec_heq (Hab ⬝ Hbc) a))
|
||||
|
|
@ -106,50 +106,42 @@ section
|
|||
H ▸ (eq.refl (Π x, P x))
|
||||
|
||||
theorem hcongr_arg (f : Πx, P x) {a b : A} (H : a = b) : f a == f b :=
|
||||
have e1 : ∀ (H : P a = P a), cast H (f a) = f a, from
|
||||
assume H, cast_eq H (f a),
|
||||
have e2 : ∀ (H : P a = P b), cast H (f a) = f b, from
|
||||
H ▸ e1,
|
||||
have e3 : cast (congr_arg P H) (f a) = f b, from
|
||||
e2 (congr_arg P H),
|
||||
eq_rec_to_heq e3
|
||||
H ▸ (heq.refl (f a))
|
||||
|
||||
-- TODO: generalize to eq_rec
|
||||
theorem cast_app' (H : P = P') (f : Π x, P x) (a : A) :
|
||||
cast (pi_eq H) f a == f a :=
|
||||
theorem rec_on_app (H : P = P') (f : Π x, P x) (a : A) : eq.rec_on H f a == f a :=
|
||||
have aux : ∀ H : P = P, eq.rec_on H f a == f a, from
|
||||
take H : P = P, heq.refl (eq.rec_on H f a),
|
||||
(H ▸ aux) H
|
||||
|
||||
theorem hcongr_fun {f : Π x, P x} {f' : Π x, P' x} (a : A) (H₁ : f == f') (H₂ : P = P') : f a == f' a :=
|
||||
have aux : ∀ (f : Π x, P x) (f' : Π x, P x), f == f' → f a == f' a, from
|
||||
take f f' H, heq.to_eq H ▸ heq.refl (f a),
|
||||
(H₂ ▸ aux) f f' H₁
|
||||
|
||||
theorem rec_on_pull (H : P = P') (f : Π x, P x) (a : A) : eq.rec_on H f a = eq.rec_on (congr_fun H a) (f a) :=
|
||||
heq.to_eq (calc
|
||||
eq.rec_on H f a == f a : rec_on_app H f a
|
||||
... == eq.rec_on (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a)))
|
||||
|
||||
theorem cast_app (H : P = P') (f : Π x, P x) (a : A) : cast (pi_eq H) f a == f a :=
|
||||
have H₁ : ∀ (H : (Π x, P x) = (Π x, P x)), cast H f a == f a, from
|
||||
assume H, heq.from_eq (congr_fun (cast_eq H f) a),
|
||||
have H₂ : ∀ (H : (Π x, P x) = (Π x, P' x)), cast H f a == f a, from
|
||||
H ▸ H₁,
|
||||
H₂ (pi_eq H)
|
||||
|
||||
-- TODO: generalize to eq_rec
|
||||
theorem cast_pull (H : P = P') (f : Π x, P x) (a : A) :
|
||||
cast (pi_eq H) f a = cast (congr_fun H a) (f a) :=
|
||||
heq.to_eq (calc
|
||||
cast (pi_eq H) f a == f a : cast_app' H f a
|
||||
... == cast (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a)))
|
||||
|
||||
theorem hcongr_fun' {f : Π x, P x} {f' : Π x, P' x} (a : A)
|
||||
(H₁ : f == f') (H₂ : P = P') : f a == f' a :=
|
||||
heq.elim H₁ (λ (Ht : (Π x, P x) = (Π x, P' x)) (Hw : cast Ht f = f'),
|
||||
calc f a == cast (pi_eq H₂) f a : heq.symm (cast_app' H₂ f a)
|
||||
... = cast Ht f a : eq.refl (cast Ht f a)
|
||||
... = f' a : congr_fun Hw a)
|
||||
|
||||
theorem hcongr' {P' : A' → Type} {f : Π a, P a} {f' : Π a', P' a'} {a : A} {a' : A'}
|
||||
theorem hcongr {P' : A' → Type} {f : Π a, P a} {f' : Π a', P' a'} {a : A} {a' : A'}
|
||||
(Hf : f == f') (HP : P == P') (Ha : a == a') : f a == f' a' :=
|
||||
have H1 : ∀ (B P' : A → Type) (f : Π x, P x) (f' : Π x, P' x), f == f' → (λx, P x) == (λx, P' x)
|
||||
have H1 : ∀ (B P' : A → Type) (f : Π x, P x) (f' : Π x, P' x), f == f' → (λx, P x) == (λx, P' x)
|
||||
→ f a == f' a, from
|
||||
take P P' f f' Hf HB, hcongr_fun' a Hf (heq.to_eq HB),
|
||||
take P P' f f' Hf HB, hcongr_fun a Hf (heq.to_eq HB),
|
||||
have H2 : ∀ (B : A → Type) (P' : A' → Type) (f : Π x, P x) (f' : Π x, P' x),
|
||||
f == f' → (λx, P x) == (λx, P' x) → f a == f' a', from heq.subst Ha H1,
|
||||
H2 P P' f f' Hf HP
|
||||
end
|
||||
|
||||
|
||||
section
|
||||
variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
|
||||
variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
|
||||
{E : Πa b c, D a b c → Type} {F : Type}
|
||||
variables {a a' : A}
|
||||
{b : B a} {b' : B a'}
|
||||
|
|
@ -157,15 +149,15 @@ section
|
|||
{d : D a b c} {d' : D a' b' c'}
|
||||
|
||||
theorem hcongr_arg2 (f : Πa b, C a b) (Ha : a = a') (Hb : b == b') : f a b == f a' b' :=
|
||||
hcongr' (hcongr_arg f Ha) (hcongr_arg C Ha) Hb
|
||||
hcongr (hcongr_arg f Ha) (hcongr_arg C Ha) Hb
|
||||
|
||||
theorem hcongr_arg3 (f : Πa b c, D a b c) (Ha : a = a') (Hb : b == b') (Hc : c == c')
|
||||
theorem hcongr_arg3 (f : Πa b c, D a b c) (Ha : a = a') (Hb : b == b') (Hc : c == c')
|
||||
: f a b c == f a' b' c' :=
|
||||
hcongr' (hcongr_arg2 f Ha Hb) (hcongr_arg2 D Ha Hb) Hc
|
||||
hcongr (hcongr_arg2 f Ha Hb) (hcongr_arg2 D Ha Hb) Hc
|
||||
|
||||
theorem hcongr_arg4 (f : Πa b c d, E a b c d)
|
||||
theorem hcongr_arg4 (f : Πa b c d, E a b c d)
|
||||
(Ha : a = a') (Hb : b == b') (Hc : c == c') (Hd : d == d') : f a b c d == f a' b' c' d' :=
|
||||
hcongr' (hcongr_arg3 f Ha Hb Hc) (hcongr_arg3 E Ha Hb Hc) Hd
|
||||
hcongr (hcongr_arg3 f Ha Hb Hc) (hcongr_arg3 E Ha Hb Hc) Hd
|
||||
|
||||
theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b')
|
||||
: f a b = f a' b' :=
|
||||
|
|
@ -176,36 +168,36 @@ section
|
|||
heq.to_eq (hcongr_arg3 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc))
|
||||
|
||||
theorem dcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b')
|
||||
(Hc : cast (dcongr_arg2 C Ha Hb) c = c')
|
||||
(Hc : cast (dcongr_arg2 C Ha Hb) c = c')
|
||||
(Hd : cast (dcongr_arg3 D Ha Hb Hc) d = d') : f a b c d = f a' b' c' d' :=
|
||||
heq.to_eq (hcongr_arg4 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))
|
||||
|
||||
--mixed versions (we want them for example if C a' b' is a subsingleton, like a proposition. Then proving eq is easier than proving heq)
|
||||
theorem hdcongr_arg3 (f : Πa b, C a b → F) (Ha : a = a') (Hb : b == b')
|
||||
(Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c')
|
||||
(Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c')
|
||||
: f a b c = f a' b' c' :=
|
||||
heq.to_eq (hcongr_arg3 f Ha Hb (eq_rec_to_heq Hc))
|
||||
|
||||
theorem hhdcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b')
|
||||
(Hc : c == c')
|
||||
(Hd : cast (dcongr_arg3 D Ha (!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hb)
|
||||
(!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hc)) d = d')
|
||||
(Hc : c == c')
|
||||
(Hd : cast (dcongr_arg3 D Ha (!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hb)
|
||||
(!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hc)) d = d')
|
||||
: f a b c d = f a' b' c' d' :=
|
||||
heq.to_eq (hcongr_arg4 f Ha Hb Hc (eq_rec_to_heq Hd))
|
||||
|
||||
theorem hddcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b')
|
||||
(Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c')
|
||||
(Hd : cast (hdcongr_arg3 D Ha Hb Hc) d = d')
|
||||
(Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c')
|
||||
(Hd : cast (hdcongr_arg3 D Ha Hb Hc) d = d')
|
||||
: f a b c d = f a' b' c' d' :=
|
||||
heq.to_eq (hcongr_arg4 f Ha Hb (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))
|
||||
|
||||
--Is a reasonable version of "hcongr2" provable without pi_ext and funext?
|
||||
--Is a reasonable version of "hcongr2" provable without pi_ext and funext?
|
||||
--It looks like you need some ugly extra conditions
|
||||
|
||||
-- theorem hcongr2' {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type} {C' : Πa, B' a → Type}
|
||||
-- {f : Π a b, C a b} {f' : Π a' b', C' a' b'} {a : A} {a' : A'} {b : B a} {b' : B' a'}
|
||||
-- (HBB' : B == B') (HCC' : C == C')
|
||||
-- {f : Π a b, C a b} {f' : Π a' b', C' a' b'} {a : A} {a' : A'} {b : B a} {b' : B' a'}
|
||||
-- (HBB' : B == B') (HCC' : C == C')
|
||||
-- (Hff' : f == f') (Haa' : a == a') (Hbb' : b == b') : f a b == f' a' b' :=
|
||||
-- hcongr' (hcongr' Hff' (sorry) Haa') (hcongr' HCC' (sorry) Haa') Hbb'
|
||||
-- hcongr (hcongr Hff' (sorry) Haa') (hcongr HCC' (sorry) Haa') Hbb'
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in a new issue