michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(builtin/kernel): move the heq axioms into kernel.lean

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-04 14:15:33 -08:00
parent 493007b7bc
commit 0283887ee9
10 changed files with 129 additions and 142 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

71
src/builtin/heq.lean
View file

@ -1,75 +1,4 @@
-- Axioms and theorems for casting and heterogenous equality
import macros
-- In the following definitions the type of A and B cannot be (Type U)
-- because A = B would be @eq (Type U+1) A B, and
-- the type of eq is (∀T : (Type U), T → T → bool).
-- So, we define M a universe smaller than U.
universe M ≥ 1
definition TypeM := (Type M)
variable cast {A B : (Type M)} : A = B → A → B
axiom cast_heq {A B : (Type M)} (H : A = B) (a : A) : cast H a == a
axiom hsymm {A B : (Type U)} {a : A} {b : B} : a == b → b == a
axiom htrans {A B C : (Type U)} {a : A} {b : B} {c : C} : a == b → b == c → a == c
axiom hcongr {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} :
f == f' → a == a' → f a == f' a'
axiom hfunext {A A' : (Type M)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} :
A = A' → (∀ x x', x == x' → f x == f' x') → f == f'
theorem hsfunext {A : (Type M)} {B B' : A → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} :
(∀ x, f x == f' x) → f == f'
:= λ Hb,
hfunext (refl A) (λ (x x' : A) (Hx : x == x'),
let s1 : f x == f' x := Hb x,
s2 : f' x == f' x' := hcongr (hrefl f') Hx
in htrans s1 s2)
theorem hallext {A A' : (Type M)} {B : A → Bool} {B' : A' → Bool}
(Ha : A = A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x)
:= boolext
(assume (H : ∀ x : A, B x),
take x' : A', (Hb (cast (symm Ha) x') x' (cast_heq (symm Ha) x')) ◂ (H (cast (symm Ha) x')))
(assume (H : ∀ x' : A', B' x'),
take x : A, (symm (Hb x (cast Ha x) (hsymm (cast_heq Ha x)))) ◂ (H (cast Ha x)))
theorem cast_app {A A' : (Type M)} {B : A → (Type M)} {B' : A' → (Type M)}
(f : ∀ x, B x) (a : A) (Ha : A = A') (Hb : (∀ x, B x) = (∀ x, B' x)) :
cast Hb f (cast Ha a) == f a
:= let s1 : cast Hb f == f := cast_heq Hb f,
s2 : cast Ha a == a := cast_heq Ha a
in hcongr s1 s2
-- The following theorems can be used as rewriting rules
theorem cast_eq {A : (Type M)} (H : A = A) (a : A) : cast H a = a
:= to_eq (cast_heq H a)
theorem cast_trans {A B C : (Type M)} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a
:= let s1 : cast Hbc (cast Hab a) == cast Hab a := cast_heq Hbc (cast Hab a),
s2 : cast Hab a == a := cast_heq Hab a,
s3 : cast (trans Hab Hbc) a == a := cast_heq (trans Hab Hbc) a,
s4 : cast Hbc (cast Hab a) == cast (trans Hab Hbc) a := htrans (htrans s1 s2) (hsymm s3)
in to_eq s4
theorem cast_pull {A : (Type M)} {B B' : A → (Type M)}
(f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) :
cast Hb f a = cast Hba (f a)
:= let s1 : cast Hb f a == f a := hcongr (cast_heq Hb f) (hrefl a),
s2 : cast Hba (f a) == f a := cast_heq Hba (f a)
in to_eq (htrans s1 (hsymm s2))
-- The following axiom is not very useful, since the resultant
-- equality is actually (@eq TypeM (∀ x, B x) (∀ x, B' x)).
-- This is the case even if A, A', B and B' live in smaller universes (e.g., Type)
-- To support this kind of axiom, it seems we have two options:
-- 1) Universe level parameters like Agda
-- 2) Axiom schema/template, where we create instances of hpiext for different universes.
-- BTW, this is essentially what Coq does since the levels are implicit in Coq.
-- axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} :
-- A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x)

76
src/builtin/kernel.lean
View file

@ -1,3 +1,6 @@
-- 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 macros
import tactic
@ -894,11 +897,70 @@ axiom pairext {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x}
(H1 : proj1 a = proj1 b) (H2 : proj2 a == proj2 b)
: a = b
-- Proof irrelevance, this is true in the set theoretic model we have for Lean.
-- In this model, the interpretation of Bool is the set {{*}, {}}.
-- Thus, if A : Bool is inhabited, then its interpretation must be {*}.
-- So, the interpretation of H1 and H2 must be *.
axiom hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
-- Heterogeneous equality axioms and theorems
-- In the following definitions the type of A and B cannot be (Type U)
-- because A = B would be @eq (Type U+1) A B, and
-- the type of eq is (∀T : (Type U), T → T → bool).
-- So, we define M a universe smaller than U.
universe M ≥ 1
definition TypeM := (Type M)
-- We can "type-cast" an A expression into a B expression, if we can prove that A = B
variable cast {A B : (Type M)} : A = B → A → B
axiom cast_heq {A B : (Type M)} (H : A = B) (a : A) : cast H a == a
-- Heterogeneous equality satisfies the usual properties: symmetry, transitivity, congruence and function extensionality
axiom hsymm {A B : (Type U)} {a : A} {b : B} : a == b → b == a
axiom htrans {A B C : (Type U)} {a : A} {b : B} {c : C} : a == b → b == c → a == c
axiom hcongr {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} {a : A} {a' : A'} :
f == f' → a == a' → f a == f' a'
axiom hfunext {A A' : (Type M)} {B : A → (Type U)} {B' : A' → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} :
A = A' → (∀ x x', x == x' → f x == f' x') → f == f'
-- Heterogeneous version of the allext theorem
theorem hallext {A A' : (Type M)} {B : A → Bool} {B' : A' → Bool}
(Ha : A = A') (Hb : ∀ x x', x == x' → B x = B' x') : (∀ x, B x) = (∀ x, B' x)
:= boolext
(assume (H : ∀ x : A, B x),
take x' : A', (Hb (cast (symm Ha) x') x' (cast_heq (symm Ha) x')) ◂ (H (cast (symm Ha) x')))
(assume (H : ∀ x' : A', B' x'),
take x : A, (symm (Hb x (cast Ha x) (hsymm (cast_heq Ha x)))) ◂ (H (cast Ha x)))
-- Simpler version of hfunext axiom, we use it to build proofs
theorem hsfunext {A : (Type M)} {B B' : A → (Type U)} {f : ∀ x, B x} {f' : ∀ x, B' x} :
(∀ x, f x == f' x) → f == f'
:= λ Hb,
hfunext (refl A) (λ (x x' : A) (Hx : x == x'),
let s1 : f x == f' x := Hb x,
s2 : f' x == f' x' := hcongr (hrefl f') Hx
in htrans s1 s2)
-- Some theorems that are useful for applying simplifications.
theorem cast_eq {A : (Type M)} (H : A = A) (a : A) : cast H a = a
:= to_eq (cast_heq H a)
theorem cast_trans {A B C : (Type M)} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (trans Hab Hbc) a
:= let s1 : cast Hbc (cast Hab a) == cast Hab a := cast_heq Hbc (cast Hab a),
s2 : cast Hab a == a := cast_heq Hab a,
s3 : cast (trans Hab Hbc) a == a := cast_heq (trans Hab Hbc) a,
s4 : cast Hbc (cast Hab a) == cast (trans Hab Hbc) a := htrans (htrans s1 s2) (hsymm s3)
in to_eq s4
theorem cast_pull {A : (Type M)} {B B' : A → (Type M)}
(f : ∀ x, B x) (a : A) (Hb : (∀ x, B x) = (∀ x, B' x)) (Hba : (B a) = (B' a)) :
cast Hb f a = cast Hba (f a)
:= let s1 : cast Hb f a == f a := hcongr (cast_heq Hb f) (hrefl a),
s2 : cast Hba (f a) == f a := cast_heq Hba (f a)
in to_eq (htrans s1 (hsymm s2))
-- Proof irrelevance is true in the set theoretic model we have for Lean.
axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
-- A more general version of proof_irrel that can be be derived using proof_irrel, heq axioms and boolext/iff_intro
theorem hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
:= let H1b : b := cast (by simp) H1,
H1_eq_H1b : H1 == H1b := hsymm (cast_heq (by simp) H1),
H1b_eq_H2 : H1b == H2 := to_heq (proof_irrel H1b H2)
in htrans H1_eq_H1b H1b_eq_H2
theorem proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
:= to_eq (hproof_irrel H1 H2)

BIN
src/builtin/obj/heq.olean
View file

Binary file not shown.

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.

14
src/kernel/kernel_decls.cpp
View file

@ -187,6 +187,18 @@ MK_CONSTANT(non_surjective_fn, name("non_surjective"));
MK_CONSTANT(ind, name("ind"));
MK_CONSTANT(infinity, name("infinity"));
MK_CONSTANT(pairext_fn, name("pairext"));
MK_CONSTANT(hproof_irrel_fn, name("hproof_irrel"));
MK_CONSTANT(TypeM, name("TypeM"));
MK_CONSTANT(cast_fn, name("cast"));
MK_CONSTANT(cast_heq_fn, name("cast_heq"));
MK_CONSTANT(hsymm_fn, name("hsymm"));
MK_CONSTANT(htrans_fn, name("htrans"));
MK_CONSTANT(hcongr_fn, name("hcongr"));
MK_CONSTANT(hfunext_fn, name("hfunext"));
MK_CONSTANT(hallext_fn, name("hallext"));
MK_CONSTANT(hsfunext_fn, name("hsfunext"));
MK_CONSTANT(cast_eq_fn, name("cast_eq"));
MK_CONSTANT(cast_trans_fn, name("cast_trans"));
MK_CONSTANT(cast_pull_fn, name("cast_pull"));
MK_CONSTANT(proof_irrel_fn, name("proof_irrel"));
MK_CONSTANT(hproof_irrel_fn, name("hproof_irrel"));
}

42
src/kernel/kernel_decls.h
View file

@ -547,10 +547,46 @@ bool is_infinity(expr const & e);
expr mk_pairext_fn();
bool is_pairext_fn(expr const & e);
inline expr mk_pairext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_pairext_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_hproof_irrel_fn();
bool is_hproof_irrel_fn(expr const & e);
inline expr mk_hproof_irrel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_hproof_irrel_fn(), e1, e2, e3, e4}); }
expr mk_TypeM();
bool is_TypeM(expr const & e);
expr mk_cast_fn();
bool is_cast_fn(expr const & e);
inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; }
inline expr mk_cast(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_fn(), e1, e2, e3, e4}); }
expr mk_cast_heq_fn();
bool is_cast_heq_fn(expr const & e);
inline expr mk_cast_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_heq_fn(), e1, e2, e3, e4}); }
expr mk_hsymm_fn();
bool is_hsymm_fn(expr const & e);
inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); }
expr mk_htrans_fn();
bool is_htrans_fn(expr const & e);
inline expr mk_htrans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_htrans_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
expr mk_hcongr_fn();
bool is_hcongr_fn(expr const & e);
inline expr mk_hcongr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8, expr const & e9, expr const & e10) { return mk_app({mk_hcongr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); }
expr mk_hfunext_fn();
bool is_hfunext_fn(expr const & e);
inline expr mk_hfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_hfunext_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
expr mk_hallext_fn();
bool is_hallext_fn(expr const & e);
inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_hsfunext_fn();
bool is_hsfunext_fn(expr const & e);
inline expr mk_hsfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hsfunext_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_cast_eq_fn();
bool is_cast_eq_fn(expr const & e);
inline expr mk_cast_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_cast_eq_fn(), e1, e2, e3}); }
expr mk_cast_trans_fn();
bool is_cast_trans_fn(expr const & e);
inline expr mk_cast_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_cast_trans_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_cast_pull_fn();
bool is_cast_pull_fn(expr const & e);
inline expr mk_cast_pull_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_cast_pull_fn(), e1, e2, e3, e4, e5, e6, e7}); }
expr mk_proof_irrel_fn();
bool is_proof_irrel_fn(expr const & e);
inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3}); }
expr mk_hproof_irrel_fn();
bool is_hproof_irrel_fn(expr const & e);
inline expr mk_hproof_irrel_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_hproof_irrel_fn(), e1, e2, e3, e4}); }
}

13
src/library/heq_decls.cpp
View file

@ -6,17 +6,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
#include "kernel/environment.h"
#include "kernel/decl_macros.h"
namespace lean {
MK_CONSTANT(TypeM, name("TypeM"));
MK_CONSTANT(cast_fn, name("cast"));
MK_CONSTANT(cast_heq_fn, name("cast_heq"));
MK_CONSTANT(hsymm_fn, name("hsymm"));
MK_CONSTANT(htrans_fn, name("htrans"));
MK_CONSTANT(hcongr_fn, name("hcongr"));
MK_CONSTANT(hfunext_fn, name("hfunext"));
MK_CONSTANT(hsfunext_fn, name("hsfunext"));
MK_CONSTANT(hallext_fn, name("hallext"));
MK_CONSTANT(cast_app_fn, name("cast_app"));
MK_CONSTANT(cast_eq_fn, name("cast_eq"));
MK_CONSTANT(cast_trans_fn, name("cast_trans"));
MK_CONSTANT(cast_pull_fn, name("cast_pull"));
}

39
src/library/heq_decls.h
View file

@ -5,43 +5,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
// Automatically generated file, DO NOT EDIT
#include "kernel/expr.h"
namespace lean {
expr mk_TypeM();
bool is_TypeM(expr const & e);
expr mk_cast_fn();
bool is_cast_fn(expr const & e);
inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; }
inline expr mk_cast(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_fn(), e1, e2, e3, e4}); }
expr mk_cast_heq_fn();
bool is_cast_heq_fn(expr const & e);
inline expr mk_cast_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_heq_fn(), e1, e2, e3, e4}); }
expr mk_hsymm_fn();
bool is_hsymm_fn(expr const & e);
inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); }
expr mk_htrans_fn();
bool is_htrans_fn(expr const & e);
inline expr mk_htrans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_htrans_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
expr mk_hcongr_fn();
bool is_hcongr_fn(expr const & e);
inline expr mk_hcongr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8, expr const & e9, expr const & e10) { return mk_app({mk_hcongr_fn(), e1, e2, e3, e4, e5, e6, e7, e8, e9, e10}); }
expr mk_hfunext_fn();
bool is_hfunext_fn(expr const & e);
inline expr mk_hfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_hfunext_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
expr mk_hsfunext_fn();
bool is_hsfunext_fn(expr const & e);
inline expr mk_hsfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hsfunext_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_hallext_fn();
bool is_hallext_fn(expr const & e);
inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_cast_app_fn();
bool is_cast_app_fn(expr const & e);
inline expr mk_cast_app_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_cast_app_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); }
expr mk_cast_eq_fn();
bool is_cast_eq_fn(expr const & e);
inline expr mk_cast_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_cast_eq_fn(), e1, e2, e3}); }
expr mk_cast_trans_fn();
bool is_cast_trans_fn(expr const & e);
inline expr mk_cast_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_cast_trans_fn(), e1, e2, e3, e4, e5, e6}); }
expr mk_cast_pull_fn();
bool is_cast_pull_fn(expr const & e);
inline expr mk_cast_pull_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_cast_pull_fn(), e1, e2, e3, e4, e5, e6, e7}); }
}

14
tests/lean/univ.lean
View file

@ -1,20 +1,20 @@
universe M >= 1
universe U >= M + 1
definition TypeM := (Type M)
universe Z ≥ M+3
universe M1 >= 1
universe U >= M1 + 1
definition TypeM1 := (Type M1)
universe Z ≥ M1+3
(*
local env = get_environment()
assert(env:get_universe_distance("Z", "M") == 3)
assert(env:get_universe_distance("Z", "M1") == 3)
assert(not env:get_universe_distance("Z", "U"))
*)
(*
local env = get_environment()
assert(env:get_universe_distance("Z", "M") == 3)
assert(env:get_universe_distance("Z", "M1") == 3)
assert(not env:get_universe_distance("Z", "U"))
*)
universe Z1 ≥ M + 1073741824.
universe Z1 ≥ M1 + 1073741824.
universe Z2 ≥ Z1 + 1073741824.
universe U1

2
tests/lean/univ.lean.expected.out
View file

@ -1,6 +1,6 @@
Set: pp::colors
Set: pp::unicode
Defined: TypeM
Defined: TypeM1
univ.lean:18:0: error: universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824
univ.lean:31:0: error: universe constraint inconsistency: U1 >= U4 + 0
univ.lean:33:0: error: invalid universe constraint: Z >= U + 0, several modules in Lean assume that U is the maximal universe