max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: automatically generate injectivity theorems

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-14 18:02:17 -07:00
parent 051ac3aef3
commit dbe0d2d706
3 changed files with 23 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Inductive.lean
View file

@ -520,8 +520,8 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
mkInductiveDecl vars views
mkSizeOfInstances view0.declName
Lean.Meta.IndPredBelow.mkBelow view0.declName
-- for view in views do
-- mkInjectiveTheorems view.declName
for view in views do
mkInjectiveTheorems view.declName
applyDerivingHandlers views
end Lean.Elab.Command

2
src/Lean/Elab/Structure.lean
View file

@ -582,7 +582,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
}
unless isClass do
mkSizeOfInstances declName
-- mkInjectiveTheorems declName
mkInjectiveTheorems declName
return declName
derivingClassViews.forM fun view => view.applyHandlers #[declName]

40
tests/lean/infoTree.lean.expected.out
View file

@ -1,6 +1,6 @@
[Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
[.] `Nat : some Sort.{?_uniq.237} @ ⟨13, 11⟩-⟨13, 14⟩
[.] `Nat : some Sort.{?_uniq.535} @ ⟨13, 11⟩-⟨13, 14⟩
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
x : Nat @ ⟨13, 7⟩-⟨13, 8⟩
Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩
@ -10,10 +10,10 @@
Prod✝ Nat Nat
Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 22⟩†
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
[.] `Nat : some Type.{?_uniq.241} @ ⟨13, 18⟩-⟨13, 21⟩
[.] `Nat : some Type.{?_uniq.539} @ ⟨13, 18⟩-⟨13, 21⟩
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
[.] `Nat : some Type.{?_uniq.240} @ ⟨13, 24⟩-⟨13, 27⟩
[.] `Nat : some Type.{?_uniq.538} @ ⟨13, 24⟩-⟨13, 27⟩
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
let y : Nat × Nat := (x, x);
id y : Nat × Nat @ ⟨14, 2⟩-⟨15, 6⟩
@ -38,16 +38,16 @@
[Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩
∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
[.] `Nat : some Sort.{?_uniq.270} @ ⟨17, 15⟩-⟨17, 18⟩
[.] `Nat : some Sort.{?_uniq.568} @ ⟨17, 15⟩-⟨17, 18⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
x : Nat @ ⟨17, 9⟩-⟨17, 10⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
[.] `Nat : some Sort.{?_uniq.272} @ ⟨17, 15⟩-⟨17, 18⟩
[.] `Nat : some Sort.{?_uniq.570} @ ⟨17, 15⟩-⟨17, 18⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
y : Nat @ ⟨17, 11⟩-⟨17, 12⟩
Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
[.] `Bool : some Sort.{?_uniq.275} @ ⟨17, 27⟩-⟨17, 31⟩
[.] `Bool : some Sort.{?_uniq.573} @ ⟨17, 27⟩-⟨17, 31⟩
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
b : Bool @ ⟨17, 23⟩-⟨17, 24⟩
x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩
@ -112,20 +112,20 @@
[Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩
Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
[.] `Nat : some Sort.{?_uniq.592} @ ⟨21, 16⟩-⟨21, 19⟩
[.] `Nat : some Sort.{?_uniq.890} @ ⟨21, 16⟩-⟨21, 19⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
x : Nat @ ⟨21, 10⟩-⟨21, 11⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
[.] `Nat : some Sort.{?_uniq.594} @ ⟨21, 16⟩-⟨21, 19⟩
[.] `Nat : some Sort.{?_uniq.892} @ ⟨21, 16⟩-⟨21, 19⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
y : Nat @ ⟨21, 12⟩-⟨21, 13⟩
Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
[.] `Bool : some Sort.{?_uniq.597} @ ⟨21, 28⟩-⟨21, 32⟩
[.] `Bool : some Sort.{?_uniq.895} @ ⟨21, 28⟩-⟨21, 32⟩
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
b : Bool @ ⟨21, 24⟩-⟨21, 25⟩
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
[.] `Nat : some Sort.{?_uniq.599} @ ⟨21, 36⟩-⟨21, 39⟩
[.] `Nat : some Sort.{?_uniq.897} @ ⟨21, 36⟩-⟨21, 39⟩
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
fun (x y : Nat) (b : Bool) =>
let x : Nat × Nat := (x + y, x - y);
@ -230,27 +230,27 @@
Prod✝ Nat (Array (Array Nat))
Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 16⟩†
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
[.] `Nat : some Type.{?_uniq.1602} @ ⟨27, 12⟩-⟨27, 15⟩
[.] `Nat : some Type.{?_uniq.1900} @ ⟨27, 12⟩-⟨27, 15⟩
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩
[.] `Array : some Type.{?_uniq.1601} @ ⟨27, 18⟩-⟨27, 23⟩
[.] `Array : some Type.{?_uniq.1899} @ ⟨27, 18⟩-⟨27, 23⟩
Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩
Macro expansion
(Array Nat)
===>
Array Nat
[.] `Array : some Type.{?_uniq.1603} @ ⟨27, 25⟩-⟨27, 30⟩
[.] `Array : some Type.{?_uniq.1901} @ ⟨27, 25⟩-⟨27, 30⟩
Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
[.] `Nat : some Type.{?_uniq.1604} @ ⟨27, 31⟩-⟨27, 34⟩
[.] `Nat : some Type.{?_uniq.1902} @ ⟨27, 31⟩-⟨27, 34⟩
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩
[.] `Array : some Sort.{?_uniq.1606} @ ⟨27, 39⟩-⟨27, 44⟩
[.] `Array : some Sort.{?_uniq.1904} @ ⟨27, 39⟩-⟨27, 44⟩
Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
[.] `Nat : some Type.{?_uniq.1607} @ ⟨27, 45⟩-⟨27, 48⟩
[.] `Nat : some Type.{?_uniq.1905} @ ⟨27, 45⟩-⟨27, 48⟩
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩
s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩
@ -264,11 +264,11 @@
Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩
[Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩
B : Type @ ⟨30, 14⟩-⟨30, 15⟩
[.] `B : some Sort.{?_uniq.1648} @ ⟨30, 14⟩-⟨30, 15⟩
[.] `B : some Sort.{?_uniq.1946} @ ⟨30, 14⟩-⟨30, 15⟩
B : Type @ ⟨30, 14⟩-⟨30, 15⟩
arg : B @ ⟨30, 8⟩-⟨30, 11⟩
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
[.] `Nat : some Sort.{?_uniq.1650} @ ⟨30, 19⟩-⟨30, 22⟩
[.] `Nat : some Sort.{?_uniq.1948} @ ⟨30, 19⟩-⟨30, 22⟩
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩
arg : B @ ⟨31, 2⟩-⟨31, 5⟩
@ -281,11 +281,11 @@
0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩
[Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
[.] `Nat : some Sort.{?_uniq.1670} @ ⟨33, 12⟩-⟨33, 15⟩
[.] `Nat : some Sort.{?_uniq.1968} @ ⟨33, 12⟩-⟨33, 15⟩
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
x : Nat @ ⟨33, 8⟩-⟨33, 9⟩
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
[.] `B : some Sort.{?_uniq.1672} @ ⟨33, 19⟩-⟨33, 20⟩
[.] `B : some Sort.{?_uniq.1970} @ ⟨33, 19⟩-⟨33, 20⟩
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
{ pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩
({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩