refactor(builtin/kernel): prove eta using function extensionality, and rename abst and abstpi to funext and allext
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
9c8026b86e
commit
a4b3d6d6c8
11 changed files with 51 additions and 45 deletions
|
|
@ -15,7 +15,7 @@ theorem subset::trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2
|
|||
in H2 x L1
|
||||
|
||||
theorem subset::ext {A : Type} {s1 s2 : Set A} (H : ∀ x, x ∈ s1 = x ∈ s2) : s1 = s2
|
||||
:= abst H
|
||||
:= funext H
|
||||
|
||||
theorem subset::antisym {A : Type} {s1 s2 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1) : s1 = s2
|
||||
:= subset::ext (have (∀ x, x ∈ s1 = x ∈ s2) :
|
||||
|
|
|
|||
|
|
@ -52,11 +52,11 @@ axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P
|
|||
|
||||
axiom iff::intro {a b : Bool} (H1 : a → b) (H2 : b → a) : a == b
|
||||
|
||||
axiom abst {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x == g x) : f == g
|
||||
-- Function extensionality
|
||||
axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x == g x) : f == g
|
||||
|
||||
axiom abstpi {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀ x : A, B x) == (∀ x : A, C x)
|
||||
|
||||
axiom eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
|
||||
-- Forall extensionality
|
||||
axiom allext {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀ x : A, B x) == (∀ x : A, C x)
|
||||
|
||||
axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
|
||||
|
||||
|
|
@ -64,6 +64,9 @@ axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
|
|||
definition substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
|
||||
:= subst H1 H2
|
||||
|
||||
theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
|
||||
:= funext (λ x : A, refl (f x))
|
||||
|
||||
theorem trivial : true
|
||||
:= refl true
|
||||
|
||||
|
|
@ -297,10 +300,10 @@ theorem not::congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b)
|
|||
:= congr2 not H
|
||||
|
||||
theorem eq::exists::intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x)
|
||||
:= congr2 (Exists A) (abst H)
|
||||
:= congr2 (Exists A) (funext H)
|
||||
|
||||
theorem not::forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x)
|
||||
:= calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not::congr (abstpi (λ x : A, symm (not::not::eq (P x))))
|
||||
:= calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not::congr (allext (λ x : A, symm (not::not::eq (P x))))
|
||||
... = (∃ x : A, ¬ P x) : refl (∃ x : A, ¬ P x)
|
||||
|
||||
theorem not::forall::elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -130,12 +130,12 @@ MK_CONSTANT(discharge_fn, name("discharge"));
|
|||
MK_CONSTANT(case_fn, name("case"));
|
||||
MK_CONSTANT(refl_fn, name("refl"));
|
||||
MK_CONSTANT(subst_fn, name("subst"));
|
||||
MK_CONSTANT(eta_fn, name("eta"));
|
||||
MK_CONSTANT(imp_antisym_fn, name({"iff", "intro"}));
|
||||
MK_CONSTANT(abst_fn, name("abst"));
|
||||
MK_CONSTANT(abst_fn, name("funext"));
|
||||
MK_CONSTANT(htrans_fn, name("htrans"));
|
||||
MK_CONSTANT(hsymm_fn, name("hsymm"));
|
||||
// Theorems
|
||||
MK_CONSTANT(eta_fn, name("eta"));
|
||||
MK_CONSTANT(trivial, name("trivial"));
|
||||
MK_CONSTANT(false_elim_fn, name({"false", "elim"}));
|
||||
MK_CONSTANT(absurd_fn, name("absurd"));
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@ Author: Soonho Kong
|
|||
#include "kernel/expr.h"
|
||||
#include "kernel/io_state.h"
|
||||
#include "kernel/builtin.h"
|
||||
#include "kernel/kernel_exception.h"
|
||||
#include "library/printer.h"
|
||||
#include "library/io_state_stream.h"
|
||||
#include "library/arith/arith.h"
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
import Int.
|
||||
axiom PlusComm(a b : Int) : a + b == b + a.
|
||||
variable a : Int.
|
||||
check (abst (fun x : Int, (PlusComm a x))).
|
||||
check (funext (fun x : Int, (PlusComm a x))).
|
||||
set::option pp::implicit true.
|
||||
check (abst (fun x : Int, (PlusComm a x))).
|
||||
check (funext (fun x : Int, (PlusComm a x))).
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@
|
|||
Imported 'Int'
|
||||
Assumed: PlusComm
|
||||
Assumed: a
|
||||
abst (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a)
|
||||
funext (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a)
|
||||
Set: lean::pp::implicit
|
||||
@abst ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) :
|
||||
@funext ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) :
|
||||
(λ x : ℤ, a + x) == (λ x : ℤ, x + a)
|
||||
|
|
|
|||
|
|
@ -5,17 +5,17 @@ variable F2 : A -> B -> C
|
|||
variable H : forall (a : A) (b : B), (F1 a b) == (F2 a b)
|
||||
variable a : A
|
||||
check eta (F2 a)
|
||||
check abst (fun a : A,
|
||||
check funext (fun a : A,
|
||||
(trans (symm (eta (F1 a)))
|
||||
(trans (abst (fun (b : B), H a b))
|
||||
(trans (funext (fun (b : B), H a b))
|
||||
(eta (F2 a)))))
|
||||
|
||||
check abst (fun a, (abst (fun b, H a b)))
|
||||
check funext (fun a, (funext (fun b, H a b)))
|
||||
|
||||
theorem T1 : F1 = F2 := abst (fun a, (abst (fun b, H a b)))
|
||||
theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := abst (fun a, (abst (fun b, H a b)))
|
||||
theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := abst (fun a, (abst (fun b, H a b)))
|
||||
theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := abst (fun a, (abst (fun b, H a b)))
|
||||
theorem T1 : F1 = F2 := funext (fun a, (funext (fun b, H a b)))
|
||||
theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := funext (fun a, (funext (fun b, H a b)))
|
||||
theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := funext (fun a, (funext (fun b, H a b)))
|
||||
theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := funext (fun a, (funext (fun b, H a b)))
|
||||
print environment 4
|
||||
set::option pp::implicit true
|
||||
print environment 4
|
||||
|
|
@ -9,35 +9,36 @@
|
|||
Assumed: H
|
||||
Assumed: a
|
||||
eta (F2 a) : (λ x : B, F2 a x) == F2 a
|
||||
abst (λ a : A, symm (eta (F1 a)) ⋈ (abst (λ b : B, H a b) ⋈ eta (F2 a))) : (λ x : A, F1 x) == (λ x : A, F2 x)
|
||||
abst (λ a : A, abst (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) == (λ (x : A) (x::1 : B), F2 x x::1)
|
||||
funext (λ a : A, symm (eta (F1 a)) ⋈ (funext (λ b : B, H a b) ⋈ eta (F2 a))) :
|
||||
(λ x : A, F1 x) == (λ x : A, F2 x)
|
||||
funext (λ a : A, funext (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) == (λ (x : A) (x::1 : B), F2 x x::1)
|
||||
Proved: T1
|
||||
Proved: T2
|
||||
Proved: T3
|
||||
Proved: T4
|
||||
theorem T1 : F1 = F2 := abst (λ a : A, abst (λ b : B, H a b))
|
||||
theorem T2 : (λ (x1 : A) (x2 : B), F1 x1 x2) = F2 := abst (λ a : A, abst (λ b : B, H a b))
|
||||
theorem T3 : F1 = (λ (x1 : A) (x2 : B), F2 x1 x2) := abst (λ a : A, abst (λ b : B, H a b))
|
||||
theorem T1 : F1 = F2 := funext (λ a : A, funext (λ b : B, H a b))
|
||||
theorem T2 : (λ (x1 : A) (x2 : B), F1 x1 x2) = F2 := funext (λ a : A, funext (λ b : B, H a b))
|
||||
theorem T3 : F1 = (λ (x1 : A) (x2 : B), F2 x1 x2) := funext (λ a : A, funext (λ b : B, H a b))
|
||||
theorem T4 : (λ (x1 : A) (x2 : B), F1 x1 x2) = (λ (x1 : A) (x2 : B), F2 x1 x2) :=
|
||||
abst (λ a : A, abst (λ b : B, H a b))
|
||||
funext (λ a : A, funext (λ b : B, H a b))
|
||||
Set: lean::pp::implicit
|
||||
theorem T1 : @eq (A → B → C) F1 F2 :=
|
||||
@abst A (λ x : A, B → C) F1 F2 (λ a : A, @abst B (λ x : B, C) (F1 a) (F2 a) (λ b : B, H a b))
|
||||
@funext A (λ x : A, B → C) F1 F2 (λ a : A, @funext B (λ x : B, C) (F1 a) (F2 a) (λ b : B, H a b))
|
||||
theorem T2 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) F2 :=
|
||||
@abst A
|
||||
(λ x : A, B → C)
|
||||
(λ (x1 : A) (x2 : B), F1 x1 x2)
|
||||
F2
|
||||
(λ a : A, @abst B (λ x : B, C) (λ x2 : B, F1 a x2) (F2 a) (λ b : B, H a b))
|
||||
@funext A
|
||||
(λ x : A, B → C)
|
||||
(λ (x1 : A) (x2 : B), F1 x1 x2)
|
||||
F2
|
||||
(λ a : A, @funext B (λ x : B, C) (λ x2 : B, F1 a x2) (F2 a) (λ b : B, H a b))
|
||||
theorem T3 : @eq (A → B → C) F1 (λ (x1 : A) (x2 : B), F2 x1 x2) :=
|
||||
@abst A
|
||||
(λ x : A, B → C)
|
||||
F1
|
||||
(λ (x1 : A) (x2 : B), F2 x1 x2)
|
||||
(λ a : A, @abst B (λ x : B, C) (F1 a) (λ x2 : B, F2 a x2) (λ b : B, H a b))
|
||||
@funext A
|
||||
(λ x : A, B → C)
|
||||
F1
|
||||
(λ (x1 : A) (x2 : B), F2 x1 x2)
|
||||
(λ a : A, @funext B (λ x : B, C) (F1 a) (λ x2 : B, F2 a x2) (λ b : B, H a b))
|
||||
theorem T4 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2) :=
|
||||
@abst A
|
||||
(λ x : A, B → C)
|
||||
(λ (x1 : A) (x2 : B), F1 x1 x2)
|
||||
(λ (x1 : A) (x2 : B), F2 x1 x2)
|
||||
(λ a : A, @abst B (λ x : B, C) (λ x2 : B, F1 a x2) (λ x2 : B, F2 a x2) (λ b : B, H a b))
|
||||
@funext A
|
||||
(λ x : A, B → C)
|
||||
(λ (x1 : A) (x2 : B), F1 x1 x2)
|
||||
(λ (x1 : A) (x2 : B), F2 x1 x2)
|
||||
(λ a : A, @funext B (λ x : B, C) (λ x2 : B, F1 a x2) (λ x2 : B, F2 a x2) (λ b : B, H a b))
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ scope
|
|||
variable hinv : B -> A
|
||||
axiom Inv (x : A) : hinv (h x) = x
|
||||
axiom H1 (x y : A) : f x y = f y x
|
||||
theorem f_eq_g : f = g := abst (fun x, (abst (fun y,
|
||||
theorem f_eq_g : f = g := funext (fun x, (funext (fun y,
|
||||
let L1 : f x y = f y x := H1 x y,
|
||||
L2 : f y x = g x y := refl (g x y)
|
||||
in trans L1 L2)))
|
||||
|
|
|
|||
|
|
@ -13,8 +13,9 @@
|
|||
Proved: Inj
|
||||
definition g (A : Type) (f : A → A → A) (x y : A) : A := f y x
|
||||
theorem f_eq_g (A : Type) (f : A → A → A) (H1 : ∀ x y : A, f x y = f y x) : f = g A f :=
|
||||
abst (λ x : A,
|
||||
abst (λ y : A, let L1 : f x y = f y x := H1 x y, L2 : f y x = g A f x y := refl (g A f x y) in L1 ⋈ L2))
|
||||
funext (λ x : A,
|
||||
funext (λ y : A,
|
||||
let L1 : f x y = f y x := H1 x y, L2 : f y x = g A f x y := refl (g A f x y) in L1 ⋈ L2))
|
||||
theorem Inj (A B : Type)
|
||||
(h : A → B)
|
||||
(hinv : B → A)
|
||||
|
|
|
|||
Loading…
Reference in a new issue