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

chore(*): minimize the use of parameters

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-09 07:13:06 -07:00
parent f9e8503005
commit 8f1b6178a7
56 changed files with 176 additions and 555 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
library/algebra/binary.lean
View file

@ -6,18 +6,18 @@ open eq.ops
namespace binary
context
parameter {A : Type}
parameter f : A → A → A
variable {A : Type}
variable f : A → A → A
infixl `*`:75 := f
definition commutative := ∀{a b}, a*b = b*a
definition associative := ∀{a b c}, (a*b)*c = a*(b*c)
end
context
parameter {A : Type}
parameter {f : A → A → A}
hypothesis H_comm : commutative f
hypothesis H_assoc : associative f
variable {A : Type}
variable {f : A → A → A}
variable H_comm : commutative f
variable H_assoc : associative f
infixl `*`:75 := f
theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) :=
take a b c, calc
@ -33,9 +33,9 @@ namespace binary
end
context
parameter {A : Type}
parameter {f : A → A → A}
hypothesis H_assoc : associative f
variable {A : Type}
variable {f : A → A → A}
variable H_assoc : associative f
infixl `*`:75 := f
theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) :=
calc

2
library/algebra/function.lean
View file

@ -4,7 +4,7 @@
namespace function
section
parameters {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
definition compose [reducible] (f : B → C) (g : A → B) : A → C :=
λx, f (g x)

4
library/data/list/basic.lean
View file

@ -19,7 +19,7 @@ namespace list
infix `::` := cons
section
parameter {T : Type}
variable {T : Type}
protected theorem induction_on {P : list T → Prop} (l : list T) (Hnil : P nil)
(Hind : ∀ (x : T) (l : list T), P l → P (x::l)) : P l :=
@ -224,7 +224,7 @@ rec_on l
-- Find
-- ----
section
parameter {H : decidable_eq T}
variable {H : decidable_eq T}
include H
definition find (x : T) : list T → nat :=

2
library/data/prod.lean
View file

@ -21,7 +21,7 @@ infixr `×` := prod
notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
section
parameters {A B : Type}
variables {A B : Type}
protected theorem destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
rec H p

4
library/data/sigma.lean
View file

@ -11,7 +11,7 @@ notation `Σ` binders `,` r:(scoped P, sigma P) := r
namespace sigma
section
parameters {A : Type} {B : A → Type}
variables {A : Type} {B : A → Type}
--without reducible tag, slice.composition_functor in algebra.category.constructions fails
definition dpr1 [reducible] (p : Σ x, B x) : A := rec (λ a b, a) p
@ -40,7 +40,7 @@ section
end
section trip_quad
parameters {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}
definition dtrip (a : A) (b : B a) (c : C a b) := dpair a (dpair b c)
definition dquad (a : A) (b : B a) (c : C a b) (d : D a b c) := dpair a (dpair b (dpair c d))

3
library/data/subtype.lean
View file

@ -13,8 +13,7 @@ notation `{` binders `,` r:(scoped P, subtype P) `}` := r
namespace subtype
section
parameter {A : Type}
parameter {P : A → Prop}
variables {A : Type} {P : A → Prop}
-- TODO: make this a coercion?
definition elt_of (a : {x, P x}) : A := rec (λ x y, x) a

7
library/data/vector.lean
View file

@ -13,7 +13,7 @@ namespace vector
notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
section sc_vector
parameter {T : Type}
variable {T : Type}
protected theorem rec_on {C : ∀ (n : ℕ), vector T n → Type} {n : ℕ} (v : vector T n) (Hnil : C 0 nil)
(Hcons : ∀(x : T) {n : ℕ} (w : vector T n), C n w → C (succ n) (cons x w)) : C n v :=
@ -35,14 +35,15 @@ namespace vector
(λa, inhabited.destruct iH
(λv, inhabited.mk (vector.cons a v))))
private theorem case_zero_lem {C : vector T 0 → Type} {n : ℕ} (v : vector T n) (Hnil : C nil) :
-- TODO(Leo): mark_it_private
theorem case_zero_lem_aux {C : vector T 0 → Type} {n : ℕ} (v : vector T n) (Hnil : C nil) :
∀ H : n = 0, C (cast (congr_arg (vector T) H) v) :=
rec_on v (take H : 0 = 0, (eq.rec Hnil (cast_eq _ nil⁻¹)))
(take (x : T) (n : ℕ) (w : vector T n) IH (H : succ n = 0),
false.rec_type _ (absurd H !succ_ne_zero))
theorem case_zero {C : vector T 0 → Type} (v : vector T 0) (Hnil : C nil) : C v :=
eq.rec (case_zero_lem v Hnil (eq.refl 0)) (cast_eq _ v)
eq.rec (case_zero_lem_aux v Hnil (eq.refl 0)) (cast_eq _ v)
private theorem rec_nonempty_lem {C : Π{n}, vector T (succ n) → Type} {n : ℕ} (v : vector T n)
(Hone : Πa, C [a]) (Hcons : Πa {n} (v : vector T (succ n)), C v → C (a :: v))

3
library/logic/axioms/examples/diaconescu.lean
View file

@ -8,9 +8,8 @@ open eq.ops nonempty inhabited
-- Diaconescu’s theorem
-- Show that Excluded middle follows from
-- Hilbert's choice operator, function extensionality and Prop extensionality
section
context
hypothesis propext {a b : Prop} : (a → b) → (b → a) → a = b
parameter p : Prop
private definition u := epsilon (λx, x = true ∨ p)

6
tests/lean/cls_err.lean
View file

@ -6,9 +6,9 @@ mk : A → H A
definition foo {A : Type} {h : H A} : A :=
H.rec (λa, a) h
section
parameter A : Type
parameter h : H A
context
variable A : Type
variable h : H A
definition tst : A :=
foo
end

4
tests/lean/interactive/proof_qed.lean
View file

@ -2,8 +2,8 @@ import logic
open eq.ops
set_option pp.notation false
section
parameter {A : Type}
parameters {a b c d e : A}
variable {A : Type}
variables {a b c d e : A}
theorem tst : a = b → b = c → c = d → d = e → a = e :=
take H1 H2 H3 H4,
have e1 : a = c,

6
tests/lean/interactive/whnfinst.lean
View file

@ -1,11 +1,11 @@
import logic
open decidable
abbreviation decidable_bin_rel {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y)
definition decidable_bin_rel {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y)
section
parameter {A : Type}
parameter (R : A → A → Prop)
variable {A : Type}
variable (R : A → A → Prop)
theorem tst1 (H : Πx y, decidable (R x y)) (a b c : A) : decidable (R a b ∧ R b a)

12
tests/lean/omit.lean
View file

@ -1,14 +1,14 @@
section
parameter A : Type
parameter a : A
parameter c : A
variable A : Type
variable a : A
variable c : A
omit A
include A
include A
omit A
parameter B : Type
parameter b : B
parameter d : B
variable B : Type
variable b : B
variable d : B
include A
include a
include c

12
tests/lean/run/algebra1.lean
View file

@ -3,10 +3,10 @@ import logic
definition Type1 := Type.{1}
context
parameter {A : Type}
parameter f : A → A → A
parameter one : A
parameter inv : A → A
variable {A : Type}
variable f : A → A → A
variable one : A
variable inv : A → A
infixl `*`:75 := f
postfix `^-1`:100 := inv
definition is_assoc := ∀ a b c, (a*b)*c = a*b*c
@ -106,8 +106,8 @@ end algebra
section
open algebra algebra.semigroup algebra.monoid
parameter M : monoid
parameters a b c : M
variable M : monoid
variables a b c : M
check a*b*c*a*b*c*a*b*a*b*c*a
check a*b
end

6
tests/lean/run/alias3.lean
View file

@ -1,8 +1,8 @@
import logic
namespace N1
section
section
context
context
parameter A : Type
definition foo (a : A) : Prop := true
check foo
@ -14,7 +14,7 @@ end N1
check N1.foo
namespace N2
section
context
parameter A : Type
inductive list : Type :=
nil {} : list,

30
tests/lean/run/basic.lean
View file

@ -9,7 +9,7 @@ definition to_carrier (g : group) := carrier g
check to_carrier.{1}
section
parameter A : Type
variable A : Type
check A
definition B := A → A
end
@ -21,9 +21,9 @@ constant a : N
check f a
section
parameter T1 : Type
parameter T2 : Type
parameter f : T1 → T2 → T2
variable T1 : Type
variable T2 : Type
variable f : T1 → T2 → T2
definition double (a : T1) (b : T2) := f a (f a b)
end
@ -39,10 +39,10 @@ check eq.{1}
section
universe l
universe u
parameter {T1 : Type.{l}}
parameter {T2 : Type.{l}}
parameter {T3 : Type.{u}}
parameter f : T1 → T2 → T2
variable {T1 : Type.{l}}
variable {T2 : Type.{l}}
variable {T3 : Type.{u}}
variable f : T1 → T2 → T2
definition is_proj2 := ∀ x y, f x y = y
definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
end
@ -52,9 +52,9 @@ check @is_proj3.{1 2}
namespace foo
section
parameters {T1 T2 : Type}
parameter {T3 : Type}
parameter f : T1 → T2 → T2
variables {T1 T2 : Type}
variable {T3 : Type}
variable f : T1 → T2 → T2
definition is_proj2 := ∀ x y, f x y = y
definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
end
@ -64,10 +64,10 @@ end foo
namespace bla
section
parameter {T1 : Type}
parameter {T2 : Type}
parameter {T3 : Type}
parameter f : T1 → T2 → T2
variable {T1 : Type}
variable {T2 : Type}
variable {T3 : Type}
variable f : T1 → T2 → T2
definition is_proj2 := ∀ x y, f x y = y
definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
end

12
tests/lean/run/bug6.lean
View file

@ -1,21 +1,21 @@
import logic
open eq
section
parameter {A : Type}
variable {A : Type}
theorem T {a b : A} (H : a = b) : b = a
:= symm H
parameters x y : A
hypothesis H : x = y
variables x y : A
variable H : x = y
check T H
check T
end
section
parameter {A : Type}
variable {A : Type}
theorem T2 ⦃a b : A⦄ (H : a = b) : b = a
:= symm H
parameters x y : A
hypothesis H : x = y
variables x y : A
variable H : x = y
check T2 H
check T2
end

42
tests/lean/run/cat.lean
View file

@ -1,42 +0,0 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn
-- category
import logic.eq logic.connectives
import data.unit data.sigma data.prod
import algebra.function
inductive category [class] (ob : Type) (mor : ob → ob → Type) : Type :=
mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
(id : Π {A : ob}, mor A A),
(Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
comp h (comp g f) = comp (comp h g) f) →
(Π {A B : ob} {f : mor A B}, comp f id = f) →
(Π {A B : ob} {f : mor A B}, comp id f = f) →
category ob mor
namespace category
precedence `∘` : 60
section
parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
definition compose := rec (λ comp id assoc idr idl, comp) Cat
definition id := rec (λ comp id assoc idr idl, id) Cat
definition ID (A : ob) := @id A
infixr `∘` := compose
theorem assoc : Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
h ∘ (g ∘ f) = (h ∘ g) ∘ f :=
rec (λ comp id assoc idr idl, assoc) Cat
theorem id_right : Π {A B : ob} {f : mor A B}, f ∘ id = f :=
rec (λ comp id assoc idr idl, idr) Cat
theorem id_left : Π {A B : ob} {f : mor A B}, id ∘ f = f :=
rec (λ comp id assoc idr idl, idl) Cat
theorem id_left2 {A B : ob} {f : mor A B} : id ∘ f = f :=
rec (λ comp id assoc idr idl, idl A B f) Cat
end
end category

11
tests/lean/run/class3.lean
View file

@ -2,13 +2,10 @@ import logic data.prod
open prod inhabited
section
parameter {A : Type}
parameter {B : Type}
parameter Ha : inhabited A
parameter Hb : inhabited B
-- The section mechanism only includes parameters that are explicitly cited.
-- So, we use the 'including' expression to make explicit we want to use
-- Ha and Hb
variable {A : Type}
variable {B : Type}
variable Ha : inhabited A
variable Hb : inhabited B
include Ha Hb
theorem tst : inhabited (Prop × A × B)

8
tests/lean/run/class5.lean
View file

@ -25,7 +25,7 @@ end nat
section
open algebra nat
parameters a b c : nat
variables a b c : nat
check a * b * c
definition tst1 : nat := a * b * c
end
@ -34,7 +34,7 @@ section
open [notation] algebra
open nat
-- check mul_struct nat << This is an error, we are open only the notation from algebra
parameters a b c : nat
variables a b c : nat
check a * b * c
definition tst2 : nat := a * b * c
end
@ -42,7 +42,7 @@ end
section
open nat
-- check mul_struct nat << This is an error, we are open only the notation from algebra
parameters a b c : nat
variables a b c : nat
check #algebra a*b*c
definition tst3 : nat := #algebra a*b*c
end
@ -53,7 +53,7 @@ section
definition add_struct [instance] : algebra.mul_struct nat
:= algebra.mul_struct.mk add
parameters a b c : nat
variables a b c : nat
check #algebra a*b*c -- << is open add instead of mul
definition tst4 : nat := #algebra a*b*c
end

2
tests/lean/run/class_bug1.lean
View file

@ -11,7 +11,7 @@ mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
class category
namespace category
section sec_cat
context sec_cat
parameter A : Type
inductive foo :=
mk : A → foo

4
tests/lean/run/class_bug2.lean
View file

@ -12,12 +12,12 @@ class category
namespace category
section sec_cat
parameter A : Type
variable A : Type
inductive foo :=
mk : A → foo
class foo
parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
variables {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
definition compose := rec (λ comp id assoc idr idl, comp) Cat
definition id := rec (λ comp id assoc idr idl, id) Cat
infixr `∘`:60 := compose

2
tests/lean/run/coesec.lean
View file

@ -2,7 +2,7 @@ inductive func (A B : Type) :=
mk : (A → B) → func A B
section
parameters {A B : Type}
variables {A B : Type}
definition to_function (F : func A B) : A → B :=
func.rec (λf, f) F
coercion to_function

4
tests/lean/run/e10.lean
View file

@ -19,8 +19,8 @@ section
open nat
open int
parameters n m : nat
parameters i j : int
variables n m : nat
variables i j : int
-- 'Most recent' are always tried first
print raw i + n

4
tests/lean/run/e11.lean
View file

@ -22,8 +22,8 @@ section
open [decls] nat
open [decls] int
parameters n m : nat
parameters i j : int
variables n m : nat
variables i j : int
check n + m
check i + j

8
tests/lean/run/group.lean
View file

@ -1,10 +1,10 @@
import logic
context
parameter {A : Type}
parameter f : A → A → A
parameter one : A
parameter inv : A → A
variable {A : Type}
variable f : A → A → A
variable one : A
variable inv : A → A
infixl `*`:75 := f
postfix `^-1`:100 := inv
definition is_assoc := ∀ a b c, (a*b)*c = a*b*c

16
tests/lean/run/group2.lean
View file

@ -1,10 +1,10 @@
import logic
context
parameter {A : Type}
parameter f : A → A → A
parameter one : A
parameter inv : A → A
variable {A : Type}
variable f : A → A → A
variable one : A
variable inv : A → A
infixl `*`:75 := f
postfix `^-1`:100 := inv
definition is_assoc := ∀ a b c, (a*b)*c = a*b*c
@ -34,10 +34,10 @@ definition mul {A : Type} {s : group_struct A} (a b : A) : A
infixl `*`:75 := mul
section
parameter G1 : group
parameter G2 : group
parameters a b c : G2
parameters d e : G1
variable G1 : group
variable G2 : group
variables a b c : G2
variables d e : G1
check a * b * b
check d * e
end

24
tests/lean/run/group3.lean
View file

@ -40,7 +40,7 @@ mk : Π mul: A → A → A,
namespace semigroup
section
parameters {A : Type} {s : semigroup A}
variables {A : Type} {s : semigroup A}
variables a b c : A
definition mul := semigroup.rec (λmul assoc, mul) s a b
context
@ -52,7 +52,7 @@ end
end semigroup
section
parameters {A : Type} {s : semigroup A}
variables {A : Type} {s : semigroup A}
include s
definition semigroup_has_mul [instance] : has_mul A := has_mul.mk semigroup.mul
@ -72,7 +72,7 @@ mk : Π (mul: A → A → A)
namespace comm_semigroup
section
parameters {A : Type} {s : comm_semigroup A}
variables {A : Type} {s : comm_semigroup A}
variables a b c : A
definition mul (a b : A) : A := comm_semigroup.rec (λmul assoc comm, mul) s a b
definition assoc : mul (mul a b) c = mul a (mul b c) :=
@ -83,7 +83,7 @@ end
end comm_semigroup
section
parameters {A : Type} {s : comm_semigroup A}
variables {A : Type} {s : comm_semigroup A}
variables a b c : A
include s
definition comm_semigroup_semigroup [instance] : semigroup A :=
@ -108,7 +108,7 @@ mk : Π (mul: A → A → A) (one : A)
namespace monoid
section
parameters {A : Type} {s : monoid A}
variables {A : Type} {s : monoid A}
variables a b c : A
include s
context
@ -127,7 +127,7 @@ namespace monoid
end monoid
section
parameters {A : Type} {s : monoid A}
variables {A : Type} {s : monoid A}
variable a : A
include s
definition monoid_has_one [instance] : has_one A := has_one.mk (monoid.one)
@ -153,7 +153,7 @@ mk : Π (mul: A → A → A) (one : A)
namespace comm_monoid
section
parameters {A : Type} {s : comm_monoid A}
variables {A : Type} {s : comm_monoid A}
variables a b c : A
definition mul := comm_monoid.rec (λmul one assoc right_id left_id comm, mul) s a b
definition one := comm_monoid.rec (λmul one assoc right_id left_id comm, one) s
@ -169,7 +169,7 @@ namespace comm_monoid
end comm_monoid
section
parameters {A : Type} {s : comm_monoid A}
variables {A : Type} {s : comm_monoid A}
include s
definition comm_monoid_monoid [instance] : monoid A :=
monoid.mk comm_monoid.mul comm_monoid.one comm_monoid.assoc
@ -183,7 +183,7 @@ end
inductive Semigroup [class] : Type := mk : Π carrier : Type, semigroup carrier → Semigroup
section
parameter S : Semigroup
variable S : Semigroup
definition Semigroup.carrier [coercion] : Type := Semigroup.rec (λc s, c) S
definition Semigroup.struc [instance] : semigroup S := Semigroup.rec (λc s, s) S
end
@ -191,21 +191,21 @@ end
inductive CommSemigroup [class] : Type :=
mk : Π carrier : Type, comm_semigroup carrier → CommSemigroup
section
parameter S : CommSemigroup
variable S : CommSemigroup
definition CommSemigroup.carrier [coercion] : Type := CommSemigroup.rec (λc s, c) S
definition CommSemigroup.struc [instance] : comm_semigroup S := CommSemigroup.rec (λc s, s) S
end
inductive Monoid [class] : Type := mk : Π carrier : Type, monoid carrier → Monoid
section
parameter S : Monoid
variable S : Monoid
definition Monoid.carrier [coercion] : Type := Monoid.rec (λc s, c) S
definition Monoid.struc [instance] : monoid S := Monoid.rec (λc s, s) S
end
inductive CommMonoid : Type := mk : Π carrier : Type, comm_monoid carrier → CommMonoid
section
parameter S : CommMonoid
variable S : CommMonoid
definition CommMonoid.carrier [coercion] : Type := CommMonoid.rec (λc s, c) S
definition CommMonoid.struc [instance] : comm_monoid S := CommMonoid.rec (λc s, s) S
end

4
tests/lean/run/ind4.lean
View file

@ -1,5 +1,5 @@
section
parameter A : Type
variable A : Type
inductive list : Type :=
nil : list,
cons : A → list → list
@ -9,7 +9,7 @@ check list.{1}
check list.cons.{1}
section
parameter A : Type
variable A : Type
inductive tree : Type :=
node : A → forest → tree
with forest : Type :=

2
tests/lean/run/indbug2.lean
View file

@ -1,6 +1,6 @@
set_option pp.implicit true
set_option pp.universes true
section
context
parameter {A : Type}
definition foo : A → A → Type := (λ x y, Type)
inductive bar {a b : A} (f : foo a b) :=

12
tests/lean/run/induniv.lean
View file

@ -3,7 +3,7 @@ nil {} : list A,
cons : A → list A → list A
section
parameter A : Type
variable A : Type
inductive list2 : Type :=
nil2 {} : list2,
cons2 : A → list2 → list2
@ -26,8 +26,8 @@ inductive group : Type :=
mk_group : Π (A : Type), (A → A → A) → A → group
section
parameter A : Type
parameter B : Type
variable A : Type
variable B : Type
inductive pair : Type :=
mk_pair : A → B → pair
end
@ -37,15 +37,15 @@ inductive eq {A : Type} (a : A) : A → Prop :=
refl : eq a a
section
parameter {A : Type}
variable {A : Type}
inductive eq2 (a : A) : A → Prop :=
refl2 : eq2 a a
end
section
parameter A : Type
parameter B : Type
variable A : Type
variable B : Type
inductive triple (C : Type) : Type :=
mk_triple : A → B → C → triple C
end

16
tests/lean/run/mor.lean
View file

@ -1,16 +0,0 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn
import algebra.category.basic
open eq eq.ops category
namespace morphism
section
parameter {ob : Type}
parameter {C : category ob}
variables {a b c d : ob} {h : hom c d} {g : hom b c} {f : hom a b}
check hom a b
end
end morphism

10
tests/lean/run/n4.lean
View file

@ -1,11 +1,11 @@
definition Prop : Type.{1} := Type.{0}
context
parameter N : Type.{1}
parameters a b c : N
parameter and : Prop → Prop → Prop
variable N : Type.{1}
variables a b c : N
variable and : Prop → Prop → Prop
infixr `∧`:35 := and
parameter le : N → N → Prop
parameter lt : N → N → Prop
variable le : N → N → Prop
variable lt : N → N → Prop
precedence `≤`:50
precedence `<`:50
infixl ≤ := le

2
tests/lean/run/one.lean
View file

@ -10,7 +10,7 @@ unit : one2
check one2
section foo
context foo
universe l2
parameter A : Type.{l2}

2
tests/lean/run/opaque_hint_bug.lean
View file

@ -4,7 +4,7 @@ cons : T → list T → list T
section
parameter {T : Type}
variable {T : Type}
definition concat (s t : list T) : list T
:= list.rec t (fun x l u, list.cons x u) s

2
tests/lean/run/sec_var.lean
View file

@ -1,6 +1,6 @@
import logic
section
context
parameter A : Type
definition foo : ∀ ⦃ a b : A ⦄, a = b → a = b :=
take a b H, H

6
tests/lean/run/secnot.lean
View file

@ -1,10 +1,10 @@
import data.num
section
parameter {A : Type}
variable {A : Type}
definition f (a b : A) := a
infixl `◀`:65 := f
parameters a b : A
variables a b : A
check a ◀ b
end
@ -14,7 +14,7 @@ cons : T → list T → list T
namespace list
section
parameter {T : Type}
variable {T : Type}
notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
check [10, 20, 30]
end

8
tests/lean/run/section1.lean
View file

@ -4,10 +4,10 @@ open tactic
section
set_option pp.universes true
set_option pp.implicit true
parameter {A : Type}
parameters {a b : A}
parameter H : a = b
parameters H1 H2 : b = a
variable {A : Type}
variables {a b : A}
variable H : a = b
variables H1 H2 : b = a
check H1
check H
check H2

8
tests/lean/run/section2.lean
View file

@ -1,17 +1,17 @@
import data.nat
section foo
parameter A : Type
variable A : Type
definition id (a : A) := a
parameter a : nat
variable a : nat
check _root_.id nat a
end foo
namespace n1
section foo
parameter A : Type
variable A : Type
definition id (a : A) := a
parameter a : nat
variable a : nat
check n1.id _ a
end foo
end n1

2
tests/lean/run/section3.lean
View file

@ -1,4 +1,4 @@
section
context
parameter (A : Type)
definition foo := A
theorem bar {X : Type} {A : X} : foo :=

4
tests/lean/run/section4.lean
View file

@ -1,10 +1,10 @@
import logic
section
context
universe k
parameter A : Type
section
context
universe l
universe u
parameter B : Type

2
tests/lean/run/set2.lean
View file

@ -8,7 +8,7 @@ definition mem {T : Type} (a : T) (s : set T) := s a = tt
infix `∈`:50 := mem
section
parameter {T : Type}
variable {T : Type}
definition empty : set T := λx, ff
notation `∅` := empty

2
tests/lean/run/simple.lean
View file

@ -1,5 +1,5 @@
definition Prop : Type.{1} := Type.{0}
section
context
parameter A : Type
definition eq (a b : A) : Prop

2
tests/lean/run/t11.lean
View file

@ -2,7 +2,7 @@ constant A : Type.{1}
constants a b c : A
constant f : A → A → A
check f a b
section
context
parameters A B : Type
parameters {C D : Type}
parameters [e d : A]

2
tests/lean/run/t4.lean
View file

@ -5,7 +5,7 @@ end foo
constant N : Type.{1}
section
parameter A : Type
variable A : Type
definition g (a : A) (B : Type) : A := a
check g.{_ 2}
end

2
tests/lean/run/t5.lean
View file

@ -12,7 +12,7 @@ namespace foo
namespace tst
print raw N N -> N
section
parameter N : Type.{4} -- Shadow previous ones.
variable N : Type.{4} -- Shadow previous ones.
print raw N
end
end tst

8
tests/lean/run/tactic29.lean
View file

@ -4,10 +4,10 @@ open tactic
section
set_option pp.universes true
set_option pp.implicit true
parameter {A : Type}
parameters {a b : A}
parameter H : a = b
parameters H1 H2 : b = a
variable {A : Type}
variables {a b : A}
variable H : a = b
variables H1 H2 : b = a
check H1
check H
check H2

6
tests/lean/run/tactic30.lean
View file

@ -4,9 +4,9 @@ open tactic
section
set_option pp.universes true
set_option pp.implicit true
parameter {A : Type}
parameters {a b : A}
parameter H : a = b
variable {A : Type}
variables {a b : A}
variable H : a = b
include H
theorem test : a = b ∧ a = a
:= by apply and.intro; assumption; apply eq.refl

4
tests/lean/run/whnfinst.lean
View file

@ -4,8 +4,8 @@ open decidable
definition decidable_bin_rel {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y)
section
parameter {A : Type}
parameter (R : A → A → Prop)
variable {A : Type}
variable (R : A → A → Prop)
theorem tst1 (H : Πx y, decidable (R x y)) (a b c : A) : decidable (R a b ∧ R b a)

317
tests/lean/slow/cat_sec_var_bug.lean
View file

@ -1,317 +0,0 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn
-- category
import logic.eq logic.connectives
import data.unit data.sigma data.prod
import algebra.function
import logic.axioms.funext
open eq eq.ops
inductive category [class] (ob : Type) : Type :=
mk : Π (hom : ob → ob → Type) (comp : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c)
(id : Π {a : ob}, hom a a),
(Π ⦃a b c d : ob⦄ {h : hom c d} {g : hom b c} {f : hom a b},
comp h (comp g f) = comp (comp h g) f) →
(Π ⦃a b : ob⦄ {f : hom a b}, comp id f = f) →
(Π ⦃a b : ob⦄ {f : hom a b}, comp f id = f) →
category ob
inductive Category : Type := mk : Π (ob : Type), category ob → Category
namespace category
section
parameters {ob : Type} {C : category ob}
variables {a b c d : ob}
definition hom : ob → ob → Type := rec (λ hom compose id assoc idr idl, hom) C
definition compose : Π {a b c : ob}, hom b c → hom a b → hom a c :=
rec (λ hom compose id assoc idr idl, compose) C
definition id : Π {a : ob}, hom a a := rec (λ hom compose id assoc idr idl, id) C
definition ID : Π (a : ob), hom a a := @id
precedence `∘` : 60
infixr `∘` := compose
infixl `=>`:25 := hom
variables {h : hom c d} {g : hom b c} {f : hom a b} {i : hom a a}
theorem assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b),
h ∘ (g ∘ f) = (h ∘ g) ∘ f :=
rec (λ hom comp id assoc idr idl, assoc) C
theorem id_left : Π ⦃a b : ob⦄ (f : hom a b), id ∘ f = f :=
rec (λ hom comp id assoc idl idr, idl) C
theorem id_right : Π ⦃a b : ob⦄ (f : hom a b), f ∘ id = f :=
rec (λ hom comp id assoc idl idr, idr) C
theorem id_compose (a : ob) : (ID a) ∘ id = id := !id_left
theorem left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id :=
calc
i = i ∘ id : symm !id_right
... = id : H
theorem right_id_unique (H : Π{b} {f : hom a b}, f ∘ i = f) : i = id :=
calc
i = id ∘ i : eq.symm !id_left
... = id : H
inductive is_section [class] (f : hom a b) : Type := mk : ∀{g}, g ∘ f = id → is_section f
inductive is_retraction [class] (f : hom a b) : Type := mk : ∀{g}, f ∘ g = id → is_retraction f
inductive is_iso [class] (f : hom a b) : Type := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
definition retraction_of (f : hom a b) {H : is_section f} : hom b a :=
is_section.rec (λg h, g) H
definition section_of (f : hom a b) {H : is_retraction f} : hom b a :=
is_retraction.rec (λg h, g) H
definition inverse (f : hom a b) {H : is_iso f} : hom b a :=
is_iso.rec (λg h1 h2, g) H
postfix `⁻¹` := inverse
theorem id_is_iso [instance] : is_iso (ID a) :=
is_iso.mk !id_compose !id_compose
theorem inverse_compose (f : hom a b) {H : is_iso f} : f⁻¹ ∘ f = id :=
is_iso.rec (λg h1 h2, h1) H
theorem compose_inverse (f : hom a b) {H : is_iso f} : f ∘ f⁻¹ = id :=
is_iso.rec (λg h1 h2, h2) H
theorem iso_imp_retraction [instance] (f : hom a b) {H : is_iso f} : is_section f :=
is_section.mk !inverse_compose
theorem iso_imp_section [instance] (f : hom a b) {H : is_iso f} : is_retraction f :=
is_retraction.mk !compose_inverse
theorem retraction_compose (f : hom a b) {H : is_section f} : retraction_of f ∘ f = id :=
is_section.rec (λg h, h) H
theorem compose_section (f : hom a b) {H : is_retraction f} : f ∘ section_of f = id :=
is_retraction.rec (λg h, h) H
theorem left_inverse_eq_right_inverse {f : hom a b} {g g' : hom b a}
(Hl : g ∘ f = id) (Hr : f ∘ g' = id) : g = g' :=
calc
g = g ∘ id : symm !id_right
... = g ∘ f ∘ g' : {symm Hr}
... = (g ∘ f) ∘ g' : !assoc
... = id ∘ g' : {Hl}
... = g' : !id_left
theorem section_eq_retraction {Hl : is_section f} {Hr : is_retraction f} :
retraction_of f = section_of f :=
left_inverse_eq_right_inverse !retraction_compose !compose_section
theorem section_retraction_imp_iso {Hl : is_section f} {Hr : is_retraction f} : is_iso f :=
is_iso.mk (subst section_eq_retraction !retraction_compose) !compose_section
theorem inverse_unique (H H' : is_iso f) : @inverse _ _ f H = @inverse _ _ f H' :=
left_inverse_eq_right_inverse !inverse_compose !compose_inverse
theorem retraction_of_id : retraction_of (ID a) = id :=
left_inverse_eq_right_inverse !retraction_compose !id_compose
theorem section_of_id : section_of (ID a) = id :=
symm (left_inverse_eq_right_inverse !id_compose !compose_section)
theorem iso_of_id : ID a⁻¹ = id :=
left_inverse_eq_right_inverse !inverse_compose !id_compose
theorem composition_is_section [instance] {Hf : is_section f} {Hg : is_section g}
: is_section (g ∘ f) :=
is_section.mk
(calc
(retraction_of f ∘ retraction_of g) ∘ g ∘ f
= retraction_of f ∘ retraction_of g ∘ g ∘ f : symm !assoc
... = retraction_of f ∘ (retraction_of g ∘ g) ∘ f : {!assoc}
... = retraction_of f ∘ id ∘ f : {!retraction_compose}
... = retraction_of f ∘ f : {!id_left}
... = id : !retraction_compose)
theorem composition_is_retraction [instance] (Hf : is_retraction f) (Hg : is_retraction g)
: is_retraction (g ∘ f) :=
is_retraction.mk
(calc
(g ∘ f) ∘ section_of f ∘ section_of g = g ∘ f ∘ section_of f ∘ section_of g : symm !assoc
... = g ∘ (f ∘ section_of f) ∘ section_of g : {!assoc}
... = g ∘ id ∘ section_of g : {!compose_section}
... = g ∘ section_of g : {!id_left}
... = id : !compose_section)
theorem composition_is_inverse [instance] (Hf : is_iso f) (Hg : is_iso g) : is_iso (g ∘ f) :=
section_retraction_imp_iso
definition mono (f : hom a b) : Prop := ∀⦃c⦄ {g h : hom c a}, f ∘ g = f ∘ h → g = h
definition epi (f : hom a b) : Prop := ∀⦃c⦄ {g h : hom b c}, g ∘ f = h ∘ f → g = h
theorem section_is_mono (f : hom a b) {H : is_section f} : mono f :=
λ C g h H,
calc
g = id ∘ g : symm !id_left
... = (retraction_of f ∘ f) ∘ g : {symm !retraction_compose}
... = retraction_of f ∘ f ∘ g : symm !assoc
... = retraction_of f ∘ f ∘ h : {H}
... = (retraction_of f ∘ f) ∘ h : !assoc
... = id ∘ h : {!retraction_compose}
... = h : !id_left
theorem retraction_is_epi (f : hom a b) {H : is_retraction f} : epi f :=
λ C g h H,
calc
g = g ∘ id : symm !id_right
... = g ∘ f ∘ section_of f : {symm !compose_section}
... = (g ∘ f) ∘ section_of f : !assoc
... = (h ∘ f) ∘ section_of f : {H}
... = h ∘ f ∘ section_of f : symm !assoc
... = h ∘ id : {!compose_section}
... = h : !id_right
end
section
definition objects [coercion] (C : Category) : Type
:= Category.rec (fun c s, c) C
definition category_instance [instance] (C : Category) : category (objects C)
:= Category.rec (fun c s, s) C
end
end category
open category
inductive functor {obC obD : Type} (C : category obC) (D : category obD) : Type :=
mk : Π (obF : obC → obD) (homF : Π⦃a b : obC⦄, hom a b → hom (obF a) (obF b)),
(Π ⦃a : obC⦄, homF (ID a) = ID (obF a)) →
(Π ⦃a b c : obC⦄ {g : hom b c} {f : hom a b}, homF (g ∘ f) = homF g ∘ homF f) →
functor C D
inductive Functor (C D : Category) : Type :=
mk : functor (category_instance C) (category_instance D) → Functor C D
infixl `⇒`:25 := functor
namespace functor
section basic_functor
variables {obC obD obE : Type} {C : category obC} {D : category obD} {E : category obE}
definition object [coercion] (F : C ⇒ D) : obC → obD := rec (λ obF homF Hid Hcomp, obF) F
definition morphism [coercion] (F : C ⇒ D) : Π{a b : obC}, hom a b → hom (F a) (F b) :=
rec (λ obF homF Hid Hcomp, homF) F
theorem respect_id (F : C ⇒ D) : Π (a : obC), F (ID a) = id :=
rec (λ obF homF Hid Hcomp, Hid) F
variable G : D ⇒ E
check respect_id G
theorem respect_comp (F : C ⇒ D) : Π ⦃a b c : obC⦄ (g : hom b c) (f : hom a b),
F (g ∘ f) = F g ∘ F f :=
rec (λ obF homF Hid Hcomp, Hcomp) F
protected definition compose (G : D ⇒ E) (F : C ⇒ D) : C ⇒ E :=
functor.mk
(λx, G (F x))
(λ a b f, G (F f))
(λ a, calc
G (F (ID a)) = G id : {respect_id F a}
... = id : respect_id G (F a))
(λ a b c g f, calc
G (F (g ∘ f)) = G (F g ∘ F f) : {respect_comp F g f}
... = G (F g) ∘ G (F f) : respect_comp G (F g) (F f))
precedence `∘∘` : 60
infixr `∘∘` := compose
protected theorem assoc {obA obB obC obD : Type} {A : category obA} {B : category obB}
{C : category obC} {D : category obD} (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
rfl
-- later check whether we want implicit or explicit arguments here. For the moment, define both
protected definition id {ob : Type} {C : category ob} : functor C C :=
mk (λa, a) (λ a b f, f) (λ a, rfl) (λ a b c f g, rfl)
protected definition ID {ob : Type} (C : category ob) : functor C C := id
protected definition Id {C : Category} : Functor C C := Functor.mk id
protected definition iD (C : Category) : Functor C C := Functor.mk id
protected theorem id_left (F : C ⇒ D) : id ∘∘ F = F := rec (λ obF homF idF compF, rfl) F
protected theorem id_right (F : C ⇒ D) : F ∘∘ id = F := rec (λ obF homF idF compF, rfl) F
end basic_functor
section Functor
variables {C₁ C₂ C₃ C₄: Category} --(G : Functor D E) (F : Functor C D)
definition Functor_functor (F : Functor C₁ C₂) :
functor (category_instance C₁) (category_instance C₂) :=
Functor.rec (λ x, x) F
protected definition Compose (G : Functor C₂ C₃) (F : Functor C₁ C₂) : Functor C₁ C₃ :=
Functor.mk (compose (Functor_functor G) (Functor_functor F))
-- namespace Functor
precedence `∘∘` : 60
infixr `∘∘` := Compose
-- end Functor
protected definition Assoc (H : Functor C₃ C₄) (G : Functor C₂ C₃) (F : Functor C₁ C₂)
: H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
rfl
protected theorem Id_left (F : Functor C₁ C₂) : Id ∘∘ F = F :=
Functor.rec (λ f, subst !id_left rfl) F
protected theorem Id_right {F : Functor C₁ C₂} : F ∘∘ Id = F :=
Functor.rec (λ f, subst !id_right rfl) F
end Functor
end functor
open functor
inductive natural_transformation {obC obD : Type} {C : category obC} {D : category obD}
(F G : functor C D) : Type :=
mk : Π (η : Π(a : obC), hom (object F a) (object G a)), (Π{a b : obC} (f : hom a b), morphism G f ∘ η a = η b ∘ morphism F f)
→ natural_transformation F G
-- inductive Natural_transformation {C D : Category} (F G : Functor C D) : Type :=
-- mk : natural_transformation (Functor_functor F) (Functor_functor G) → Natural_transformation F G
infixl `==>`:25 := natural_transformation
namespace natural_transformation
section
parameters {obC obD : Type} {C : category obC} {D : category obD} {F G : C ⇒ D}
definition natural_map [coercion] (η : F ==> G) :
Π(a : obC), hom (object F a) (object G a) :=
rec (λ x y, x) η
definition naturality (η : F ==> G) :
Π{a b : obC} (f : hom a b), morphism G f ∘ η a = η b ∘ morphism F f :=
rec (λ x y, y) η
end
section
parameters {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D}
protected definition compose (η : G ==> H) (θ : F ==> G) : F ==> H :=
natural_transformation.mk
(λ a, η a ∘ θ a)
(λ a b f,
calc
morphism H f ∘ (η a ∘ θ a) = (morphism H f ∘ η a) ∘ θ a : !assoc
... = (η b ∘ morphism G f) ∘ θ a : {naturality η f}
... = η b ∘ (morphism G f ∘ θ a) : symm !assoc
... = η b ∘ (θ b ∘ morphism F f) : {naturality θ f}
... = (η b ∘ θ b) ∘ morphism F f : !assoc)
end
precedence `∘n` : 60
infixr `∘n` := compose
end natural_transformation

2
tests/lean/slow/list_elab2.lean
View file

@ -31,7 +31,7 @@ infix `::` : 65 := cons
section
parameter {T : Type}
variable {T : Type}
theorem list_induction_on {P : list T → Prop} (l : list T) (Hnil : P nil)
(Hind : forall x : T, forall l : list T, forall H : P l, P (cons x l)) : P l :=

2
tests/lean/t4.lean
View file

@ -13,7 +13,7 @@ constant f (a b : N) : N
constant len.{l} (A : Type.{l}) (n : N) (v : vec.{l} A n) : N
check f
check len.{1}
section
context
parameter A : Type
parameter B : Prop
hypothesis H : B

4
tests/lean/t6.lean
View file

@ -1,7 +1,7 @@
definition Prop : Type.{1} := Type.{0}
section
parameter {A : Type} -- Mark A as implicit parameter
parameter R : A → A → Prop
variable {A : Type} -- Mark A as implicit parameter
variable R : A → A → Prop
definition id (a : A) : A := a
definition refl : Prop := forall (a : A), R a a
definition symm : Prop := forall (a b : A), R a b -> R b a

2
tests/lean/t7.lean
View file

@ -1,6 +1,6 @@
definition Prop : Type.{1} := Type.{0}
constant and : Prop → Prop → Prop
section
context
parameter {A : Type} -- Mark A as implicit parameter
parameter R : A → A → Prop
parameter B : Type

2
tests/lean/var.lean
View file

@ -1,7 +1,7 @@
import logic
section
context
variable A : Type
parameter a : A
end

2
tests/lean/var2.lean
View file

@ -1,7 +1,7 @@
import logic
section
context
universe l
variable A : Type.{l}
variable a : A