subst.eq

Stream: general

[Michael Beeson]

The following example generates errors in its last line. I do not understand why. Can someone please correct those lines for me?
If we have a proof that x ∈ single y and by definition single x = pair x x then we want to conclude x ∈ pair y y.

import init
constant M : Type
set_option default_priority 100
reserve infix ` ∈ ` : 49
constant mem : M → M → Prop
variables x y z: M
infix ∈ := mem
constant single: M → M
constant pair: M → M → M
constant single_definition: ∀ x, (single x = pair x x)
#check single_definition y  /- single y = pair y y -/
constant h: x ∈ single y
#check eq.subst (single_definition y) h
``` lean

[Yury G. Kudryashov]

Please use ```lean

[Johan Commelin]

Pro tip:

```lean
code goes here
```

gives you syntax highlighting

[Michael Beeson]

(deleted)

[Michael Beeson]

(deleted)

[Yury G. Kudryashov]

```lean

```

[Yury G. Kudryashov]

three backquotes lean<RET>code<RET>three backquotes

[Michael Beeson]

(deleted)

[Yury G. Kudryashov]

Also you can edit old posts instead of creating new ones

[Michael Beeson]

import init
constant M : Type
set_option default_priority 100
reserve infix ` ∈ ` : 49
constant mem : M → M → Prop
variables x y z: M
infix ∈ := mem
constant single: M → M
constant pair: M → M → M
constant single_definition: ∀ x, (single x = pair x x)
#check single_definition y  /- single y = pair y y -/
constant h: x ∈ single y
#check eq.subst (single_definition y) h

[Michael Beeson]

How do I edit (or in this case delete) old posts?

[Patrick Massot]

There is a drop-down menu near the time stamp in the top-right corner

[Patrick Massot]

Or the keybinding is e (if you are not editing a message of course)

[Kevin Buzzard]

You don't need import init, it's imported automatically

[Yury G. Kudryashov]

Try example : x ∈ pair y y := single_definition y ▸ h x y instead of #check

[Patrick Massot]

And your Lean code is very weird

[Yury G. Kudryashov]

E.g. it says that any x belongs to singleton y for any y

[Johan Commelin]

@Michael Beeson Welcome! Can you tell us a little bit about the "background" for your question? What are you trying to achieve?

[Johan Commelin]

Also, what tutorials/books have you followed?

[Patrick Massot]

If you are coming from another proof assistant you should probably spend some time learning and asking basic questions.

[Yury G. Kudryashov]

Probably you want

example (h : x ∈ single y) : x ∈ pair y y := single_definition y ▸ h

instead of the last 2 lines.

[Yury G. Kudryashov]

Note that constant defines a universal constant with no known properties (apart from those defined by axioms)

[Yury G. Kudryashov]

In particular, you will not be able to apply any lemmas you prove in your file, e.g., to nat.

[Yury G. Kudryashov]

Or anything but M.

[Yury G. Kudryashov]

If you want to have theorems/definitions that work for any Type, you should use variable (M : Type*) instead.

[Michael Beeson]

I am reading Theorem Proving in Lean. I'm trying with this example to understand eq.subst. This is taken from a finite axiomatization of
intuitionistic NF set theory that I'm formalizing in Lean as an introductory exercise. I thought this WAS a basic question.

[Michael Beeson]

Yes, that's the intention, this is a first-order theory with model carried by M.

[Kevin Buzzard]

It looks like a fine basic question to me. In Lean we essentially never use constants and axioms.

[Michael Beeson]

I know, but that's one way to do first-order logic in Lean. There should be another way, using a class declaration, but the part of the manual I needed for that is apparently not written yet, so I went this route instead. It is adequate.

[Michael Beeson]

You never use constants and axioms in formalizing libraries of mathematics, of course, but this is not what I'm doing here, I'm formalizing a first-order theory.

[Yury G. Kudryashov]

You can use

structure Model :=
(M : Type*)
(single : M → M)
(pair : M → M → M)
(single_def : ∀ x, single x = pair x x)

[Yury G. Kudryashov]

You can add more data and axioms

[Michael Beeson]

I tried essentially that with "class" instead of structure.

[Yury G. Kudryashov]

With class you'll need something like

class Model (M : Type*) := (single : M → M) ...

variables (M : Type*) [Model M]

[Michael Beeson]

It complained that I'm not allowed "variables" inside a class.
That's when I switched to the other approach.

[Yury G. Kudryashov]

Then you can #check Model.single and #check Model.pair to see what arguments explicit/implicit.

[Yury G. Kudryashov]

You don't declare variables inside a class. You list fields using the same syntax as for structure but move M to the argument.

[Yury G. Kudryashov]

The error about subst.eq means the following. When you write subst.eq h a, Lean wants to know (a) the type of h (including all implicit args); (b) the type of your goal.

[Yury G. Kudryashov]

So, it will never work with #check unless you use something like show ..., from eq.subst h a

[Michael Beeson]

OK. Thank you, Yury, for these helpful lessons. I'll rework my code tomorrow .

[Michael Beeson]

The following code generates an error if you uncomment the commented line.
On the other hand if you uncomment the commented line and comment out the next line then
it also generates an error. So it looks like either of the last two lines is OK by itself but not together.
What is going on here? Also, why does my section name have to be the same as my class name and both
are ended together with one end command?

set_option default_priority 100
reserve infix ` ∈ ` : 49
section Model
class  Model (M:Type) :=
(mem : M → M → Prop)
/-infix ∈ := Model.binary_union-/
(extensionality_axiom:  ∀ a b, (∀ x, (mem x a ↔ mem x b) → a=b))
end Model

[Alex J. Best]

The class consists of several fields, mem and extensionality_axiom in this case, the next line which isnt of the form (name : Type) is ending the definition of the class here, so when you uncomment the infix line lean thinks you are done with that class.
The end Model only applies to the section, and doesn't need to have the same name as the class.

set_option default_priority 100
reserve infix ` ∈ ` : 49
section Moodel
class  Model (M:Type) :=
(mem : M → M → Prop)
(extensionality_axiom:  ∀ a b, (∀ x, (mem x a ↔ mem x b) → a=b))

infix ∈ := Model.binary_union
end Moodel

[Alex J. Best]

The infix doesn't work as lean doesn't know what Model.binary_union is btw.

[Michael Beeson]

Thanks, I understand the answer. Now, where can I put the infix declaration so it will work? Not before the class, since it won't know what Model.mem is there. Not after the class, at least, if I want to use the infix notation inside the class. And, not inside the class,
since that will terminate the class definition. um, where then?

[Alex J. Best]

You can do it like this

class  Model (M:Type) :=
(mem : M → M → Prop)
(infix ` ∈ `:1001 := mem)
(extensionality_axiom:  ∀ a b, (∀ x, ( x ∈ a ↔ x ∈ b) → a=b))

[Kenny Lau]

it still isn't bracketed right btw

[Alex J. Best]

The extensionality yeah?

[Kenny Lau]

yeah

[Alex J. Best]

Also I believe you have to redeclare the notation if you want to use it outside of the class as in

section Model

class  Model (M:Type) :=
(mem : M → M → Prop)
(infix ` ∈ `:1001 := mem)
(extensionality_axiom : ∀ a b, (∀ x, (x ∈ a ↔ x ∈ b) → a=b))

variables (M : Type) [Model M] (a b : M)

open Model
#check extensionality_axiom
infix ` ∈ ` := Model.mem
#check a ∈ b

end Model

[Michael Beeson]

oh, oops about the bracketing. But having binary_union in place of mem is just a cut-and-paste error
as the actual file has mem there.

[Michael Beeson]

I don't seem to have to redeclare the infix notation, probably because at the top of my file I have

set_option default_priority 100
reserve infix ` ∈ ` : 49
reserve infix ` ⊆ ` : 49
reserve infix ` ∪ ` : 50
reserve infix ` ∩ ` : 50
reserve infix ` × ` : 50

[Michael Beeson]

But I do definitely need the second "open Model". Now I have two "open Model" and only one "end Model". I don't understand
why I need the second "open Model".

[Michael Beeson]

Also if I try to include the line

(@[simp] single_definition: ∀ x, (single x = pair x x) )

it causes an error, while without "@[simp]" all is fine.

[Alex J. Best]

Where is your second open Model? If you have a section called model and then a class inside it called Model then in order to refer to fields of the class Model by their name, instead of Model.name you can run open Model. I don't see the need for two (unless you are in a different section).

[Alex J. Best]

section name pairs with end name, and open is something different, I'd rename your section to something else (even just models to make the names not overlap personally.

[Michael Beeson]

Here is an initial segment of my file showing the two open Model commands.
Well actually the first one is not an "open" command but a section command.

set_option default_priority 100
reserve infix ` ∈ ` : 49
reserve infix ` ⊆ ` : 49
reserve infix ` ∪ ` : 50
reserve infix ` ∩ ` : 50
reserve infix ` × ` : 50

section Model
class  Model (M:Type) :=
(mem : M → M → Prop)
(subset: M → M → Prop)
(phi : M)
(c: M → M)
(V: M)
(binary_union : M → M → M)
(union: M → M)
(intersection : M → M → M)
(imp: M → M → M)
(pair: M → M → M)
(single: M → M)
(ordered_pair: M → M → M)
(product: M → M → M)
(Rel: M →  Prop)
(dom: M → M)
(inv: M → M )
(join: M → M → M)
(SI: M → M )  /- singleton_image -/
(subset_relation: M)
(equality_relation: M)
(proj1: M)
(proj2: M)
( single_definition : ∀ x, single x = pair x x)
(infix  ∈ :=  mem )
(infix ∪ := binary_union)
(infix ∩ := intersection)
(infix × := product)
(infix ⊆ := subset)
(extensionality_axiom:  ∀ a b, (∀ x, (x ∈ a ↔ x ∈ b)) → a=b)
(binary_union_axiom:   ∀ a b x, (x ∈ a ∪ b ↔ x ∈ a ∨  x ∈ b))
(intersection_axiom:  ∀ a b x, (x ∈ a ∩  b ↔ x ∈ a ∧  x ∈ b))
(complement_axiom:  ∀ a x, (x ∈ c a ↔ ¬ x ∈ a))
(implication_axiom:    ∀ a b x, (x ∈ imp a b ↔ (x ∈ a → x ∈ b)))
(emptyset_axiom:   ∀ x, (¬ x ∈ phi))
(pairing_axiom:  ∀ x a b, (x ∈ pair a b  ↔ (x = a ∨  x = b)))
(ordered_pairing_axiom:   ∀ x y, (ordered_pair x y  = pair x (pair x y)))
(domain:  ∀ R, (Rel R → ∀ x, (x ∈ dom R ↔ ∃ y, (ordered_pair x y  ∈ R))))
(V_definition:   ∀ x, ( x ∈ V))
(Rel_definition:  ∀ X, ( Rel X ↔ ∀ z, (z ∈ X →  ∃ a b,(z = ordered_pair a b))))
(product_axiom:   ∀ x y u, (u ∈ x × y ↔ ∃ a b, (a ∈ x ∧ b ∈ y ∧ u = ordered_pair a b )))
(inverse_axiom:   ∀ R, (Rel R → ∀ x y, (ordered_pair x y ∈ inv R ↔ ordered_pair y x ∈ R)))
(equality_relation_axiom:  ∀ x, ( x ∈ equality_relation ↔ ∃ z, (x = ordered_pair z z )))
(subset_definition:   ∀ x y, (x ⊆ y ↔ ∀ z, (z ∈ x → z ∈ y)))
(subset_relation_axiom:  ∀ x y, (ordered_pair x y  ∈ subset_relation ↔ x ⊆ y))
 (union_axiom:   ∀ x y, (x ∈ union y ↔ ∃ z, (z ∈ y ∧ x ∈ z)))

 /- end of class definition because next line doesn't declare a member -/

variables (M:Type) [Model M] (a b x y z u v w X R W: M)

open Model
#check extensionality_axiom



end Model

[Alex J. Best]

I only see one open Model!

[Michael Beeson]

Yes, but doesn't the section Model command have the effect of opening the section?

[Alex J. Best]

Michael Beeson said:

Also if I try to include the line

(@[simp] single_definition: ∀ x, (single x = pair x x) )

it causes an error, while without "@[simp]" all is fine.

you won't need to tag these definitions with simp, the tag @[simp] can be used on lemmas or theorems to make the simplifier try to apply them in later proofs.

[Alex J. Best]

Yes, the open Model command refers to the class Model here

[Michael Beeson]

So maybe it's crazy to name the section and the class both Model.

[Alex J. Best]

Without it you can't refer to extensionality_axiom without prefixing it Model.extensionality_axiom, its a convenience thing only.

[Michael Beeson]

So you can "open" either a section or a class, and you can "end" a section. I can't, however, either "close" or "end" a class afer opening it.

[Michael Beeson]

Oh wait, maybe you can't "open" a section; only a class.

[Kevin Buzzard]

You are not using any of the functionality of sections, and if you don't really know what they are then it might be best to remove section Model and end Model completely. I don't know what you think they're doing, but they are just some organisational principle for managing variables in a principled manner, and in particular section Model/end Model may as well say section xyzzy/end xyzzy; they do not affect your Model class in any way.

[Kevin Buzzard]

sections

[Michael Beeson]

What I thought they were doing was limiting the scope of my variables to the section.

[Kevin Buzzard]

Right.

[Michael Beeson]

But regardless of sections, there must be a way to undo the effect of "opening" a class.

[Kevin Buzzard]

But given that you don't have anything going on outside the section, or any reason to limit the scope of the variables to any subset of your code right now, why not just remove it for now?

[Kevin Buzzard]

I don't know what you think "opening" a class means, but open foo simply means that you no longer have to type foo.bar, you can just type bar instead.

[Michael Beeson]

I put a section command in just in accordance with the general principle that global variables are bad, bad, bad.

[Kevin Buzzard]

I don't think that these are the kind of variables for which that principle holds.

[Michael Beeson]

Well it doesn't matter anyway as this is never going to be more than a one-file project.

[Kevin Buzzard]

You are not really globally defining X to mean anything when you write variable (X : foo), you're just telling Lean that if it sees an X in the middle of a definition and you didn't bother saying what it was, then it's a foo.

[Michael Beeson]

Well, if six months from now in another file I forget to declare X and I have inputted this file then Lean will infer the wrong type for X and I might waste an hour figuring out what's going on.

[Kevin Buzzard]

That is not true. That's what I'm saying.

[Marc Huisinga]

from the code i've seen, sections are mostly used for managing variable commands, and namespaces are mostly used for avoiding global variables (https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#namespaces)

[Kevin Buzzard]

variable (X : bool)

example (X : ℤ) : 2 * X = X + X := two_mul X -- here X is an integer

example : X = X := rfl -- here it's a bool, but only because we didn't say what it was

[Kevin Buzzard]

If you import this file in another file then variable (X : bool) will no longer apply, and if you use X without saying what it is you'll get an error. variable is just a local trick in a file to save you having to always say that X is a bool in the theorems you're proving in this file

[Kevin Buzzard]

It's more a device to save typing than anything else.

[Michael Beeson]

Aha! So to speak, all "variable declarations" are static, in the sense that their scope is limited to a file.

That has the possibly nasty effect that "input foo" is not the same thing as pasting the contents of foo where you
have the input command.

[Kevin Buzzard]

Lean has a set-up for handling notation, and it's not what you are using.

[Kevin Buzzard]

There is no input command, there is only an import command, and it can only take place at the very top of the file, so this is not an issue.

[Michael Beeson]

I mean "import".

Now if file1 has a variable declaration of X and file2 has "import file1" then the declaration of X
will not have effect in file 2. But if I replace the import command with the contents of file 1 then
the declaration of X will have effect in file 2.

[Michael Beeson]

Regarding "Lean has a way and I'm not using it", I'm here on Zulip to learn Lean, so please point me in the right direction.

[Kevin Buzzard]

class Model (M:Type) extends has_mem M M, has_subset M, has_union M, has_inter M :=
(phi : M)
(c: M → M)
(V: M)
...

[Kevin Buzzard]

binary_union is called union, and union is called Union

[Michael Beeson]

Well, but I'm trying to write a self-contained first-order theory. I don't want to import any axioms from elsewhere about the primitive symbols.

[Kevin Buzzard]

There are no axioms. The things you're extending are just notation.

[Michael Beeson]

So your point is that by using extends has_mem, I could avoid the need to declare (infix ∈ := mem ) ?

[Kevin Buzzard]

Right -- has_mem has done all that for you.

[Michael Beeson]

But "(infix ∈ := mem )" is not longer than "extends has_mem"

[Michael Beeson]

But anyway, I understand now that I could do it that way, thanks.

[Kevin Buzzard]

The advantage of doing it the way I'm suggesting is that you can use the notation immediately, even in the axioms for your class.

[Michael Beeson]

But I did use it in the axioms, by putting the axioms after the (infix ∈ := mem ) lines (once someone showed me how to do that inside the class.

[Kevin Buzzard]

I have no idea whether that will work in practice. I have never seen anyone declare infix notation within a class before.

[Michael Beeson]

Well, it seems to work. Thanks to the wizards here on Zulip.
Anyway now I have TWO ways to do it so I am double happy.

[Michael Beeson]

There are however other things that I do not know even ONE way to do. For example use notation {a, b} for pair a b.
This has something to do with "foldr" and I stared at the example in TPIL quite a while but could not make it work.
So can we do that too with "extends" ?

[Kevin Buzzard]

That notation is already taken in Lean, so it will be touch and go if you try to redefine it.

[Kevin Buzzard]

Actually, it already means more than one thing, so maybe it will be fine ;-)

[Marc Huisinga]

the foldr example is the one for lists, right?

[Michael Beeson]

Yes, that's the example I was staring at.

[Alex J. Best]

I think the extends way will require less typing in the long run, you won't have to redeclare the notation to use it later. When I tried it I had to help lean with the types a bit more though: e.g.

section Model

class Model (M : Type) extends has_mem M M :=
(extensionality_axiom : ∀ a b : M, (∀ x, (x ∈ a ↔ x ∈ b)) → a=b) -- I had to add : M after a b here

variables (M : Type) [Model M] (a b : M)

open Model
#check extensionality_axiom
#check a ∈ b

end Model

[Marc Huisinga]

in that case the notation is a bit more involved because lists can have arbitrary length. for pairs you can get away with less involved notation commands.

[Marc Huisinga]

it has been a while since i have fiddled with notation, and getting the priorities right is always a bit tricky ...

[Michael Beeson]

Anyway this is not a serious problem for me. I'm fine with typing "pair a b" instead of {a, b} for the duration of this exercise.

[Marc Huisinga]

taking your example from above, this works (for pair):

section Model
class  Model (M:Type) :=
(mem : M → M → Prop)
(subset: M → M → Prop)
(phi : M)
(c: M → M)
(V: M)
(binary_union : M → M → M)
(union: M → M)
(intersection : M → M → M)
(imp: M → M → M)
(pair: M → M → M)
(single: M → M)
(ordered_pair: M → M → M)
(product: M → M → M)
(Rel: M →  Prop)
(dom: M → M)
(inv: M → M )
(join: M → M → M)
(SI: M → M )  /- singleton_image -/
(subset_relation: M)
(equality_relation: M)
(proj1: M)
(proj2: M)
(single_definition : ∀ x, single x = pair x x)
(infix ∈ := mem )
(infix ∪ := binary_union)
(infix ∩ := intersection)
(infix × := product)
(infix ⊆ := subset)
(notation `{` a `,` b `}` := pair a b)
(extensionality_axiom:  ∀ a b, (∀ x, (x ∈ a ↔ x ∈ b)) → a=b)
(binary_union_axiom:   ∀ a b x, (x ∈ a ∪ b ↔ x ∈ a ∨  x ∈ b))
(intersection_axiom:  ∀ a b x, (x ∈ a ∩  b ↔ x ∈ a ∧  x ∈ b))
(complement_axiom:  ∀ a x, (x ∈ c a ↔ ¬ x ∈ a))
(implication_axiom:    ∀ a b x, (x ∈ imp a b ↔ (x ∈ a → x ∈ b)))
(emptyset_axiom:   ∀ x, (¬ x ∈ phi))
(pairing_axiom:  ∀ x a b, (x ∈ {a, b} ↔ (x = a ∨ x = b)))
(ordered_pairing_axiom:   ∀ x y, (ordered_pair x y = {x, {x, y}}))
(domain:  ∀ R, (Rel R → ∀ x, (x ∈ dom R ↔ ∃ y, (ordered_pair x y ∈ R))))
(V_definition:   ∀ x, (x ∈ V))
(Rel_definition:  ∀ X, ( Rel X ↔ ∀ z, (z ∈ X →  ∃ a b,(z = ordered_pair a b))))
(product_axiom:   ∀ x y u, (u ∈ x × y ↔ ∃ a b, (a ∈ x ∧ b ∈ y ∧ u = ordered_pair a b )))
(inverse_axiom:   ∀ R, (Rel R → ∀ x y, (ordered_pair x y ∈ inv R ↔ ordered_pair y x ∈ R)))
(equality_relation_axiom:  ∀ x, ( x ∈ equality_relation ↔ ∃ z, (x = ordered_pair z z )))
(subset_definition:   ∀ x y, (x ⊆ y ↔ ∀ z, (z ∈ x → z ∈ y)))
(subset_relation_axiom:  ∀ x y, (ordered_pair x y  ∈ subset_relation ↔ x ⊆ y))
 (union_axiom:   ∀ x y, (x ∈ union y ↔ ∃ z, (z ∈ y ∧ x ∈ z)))

not sure if this works well, though.

[Michael Beeson]

Great! Thank you very much! That is cool. No "foldr" involved.

[Marc Huisinga]

yes, the foldr handles lists of arbitrary lengths

[Andrew Ashworth]

is intuitionistic NF set theory this? http://us.metamath.org/nfeuni/mmnf.html

[Michael Beeson]

Andrew Ashworth said:

is intuitionistic NF set theory this? http://us.metamath.org/nfeuni/mmnf.html

No, that is a finite axiomatization of classical NF. If you want to know what NF is, look it up in Wikipedia or the Stanford Encyclopedia of Philosophy. Intuitionistic NF is simply NF with only intuitionistic logic.

[Michael Beeson]

Now I guess I have everything working. Here is a small sample. You will see that I had to repeat the notation command outside the class; if you remove it it doesn't work. Also inside the classs it needs to be in parentheses and outside the class it may not be in parentheses. God knows why. Anyway, this file and the larger file from which I abstracted it is working. Now, I can move on to my original question about subst.eq for which this topic is named. But not in this message.

set_option default_priority 100
reserve infix ` ∈ ` : 49
class  Model (M:Type) :=
(mem : M → M → Prop)
(pair: M → M → M)
(single: M → M)
(infix  ∈  :=  mem )
(notation `{` a `,` b `}` := pair a b)
(extensionality_axiom:  ∀ a b, (∀ x, (mem x a ↔ mem x b)) → a=b)
( single_definition : ∀ x, single x = {x,x})
(notation `{` a `,` b `}` := pair a b)

open Model
variables (M:Type) [Model M] (a b x y z u v w X R W: M)

#check eq.symm(single_definition x)

notation `{` a `,` b `}` := pair a b
lemma single_definition_reverse : ∀ x:M, {x,x}  = single x :=
   λ x, eq.symm(single_definition x)

[Scott Morrison]

I'd advise not attempting to use { ... , ... } in custom notation. The core parser has special handling for braces, and you are just going to suffer down the line.

[Mario Carneiro]

If you want to use the braces notation, you should try to do it by implementing has_insert and has_emptyc instead

[Michael Beeson]

Two questions about the following code: (1) Why after the declaration of constant h does #check not return the type of h just declared
but instead the more complicated type in the next line?

The original post asked a further question which I have since withdrawn. (It was dumb.)
But I'd still like question (1) answered.

set_option default_priority 100
reserve infix ` ∈ ` : 49
class  Model (M:Type)  :=
(mem : M → M → Prop)
(pair: M → M → M)
(single: M → M)
(infix  ∈  :=  mem )
(notation `{` a `,` b `}` := pair a b)
(extensionality_axiom:  ∀ a b, (∀ x, (mem x a ↔ mem x b)) → a=b)
(pairing_axiom:  ∀ x a b, (x ∈ {a,b} ↔ (x = a ∨  x = b)))
( single_definition : ∀ x, single x = {x,x})
(notation `{` a `,` b `}` := pair a b)

open Model
infix  ∈ :=  mem
notation `{` a `,` b `}` := pair a b
variables (M:Type) [Model M] (a b x y z u v w X R W: M)

#check eq.symm(single_definition x)
lemma single_definition_reverse : ∀ x:M, {x,x}  = single x :=
   λ x, eq.symm(single_definition x)

#check single_definition x

constant h: x ∈ single y
#check h
#check h M x y
example : x ∈ {y,y} := single_definition y ▸ h M x y

[Michael Beeson]

OK but notation is not the issue here. If I take out the braces and just use pair I will still have the problem with not
understanding the type of h.

[Michael Beeson]

And besides I am not going "down the line" very far with this. I'm only going to prove a few theorems in this one file to see what
I can learn. And it's easier to read the familiar notation {x,y} for unordered pair.

[Michael Beeson]

The first question I asked, how to prove x \in {x,x}, I've deleted. You don't have x \in single x to
work with . That will only be available AFTER you prove x \in {x,x} from the pairing axiom. So never mind
that now-deleted question.

[Mario Carneiro]

Your constant h pulls in the variables x and y from the variables line in order to produce a universally quantified axiom asserting that x \in single y for all x and y, which is certainly not what you want

[Mario Carneiro]

You should let h be a variable too

[Michael Beeson]

I don't want to keep that line more than a few minutes, or however long it takes to understand Lean's response. It's not for any other purpose.

[Mario Carneiro]

that's what variable is for

[Mario Carneiro]

constant is basically a synonym of axiom

[Mario Carneiro]

and it is easy to accidentally write inconsistent axioms so we try to avoid these commands entirely

[Mario Carneiro]

If you want to scope your variable declarations to a portion of the file, use section ... end

[Michael Beeson]

So if I write 'variable' instead of 'constant' there then Lean responds to the check as I expected, differently than with 'constant'.

[Mario Carneiro]

If you want a temporary notation, use local notation instead of notation. This will override all other uses of the notation, so you probably won't be able to use {x | p x} or {x // p x} or {x, y, z} on sets, finsets and other such things, until the end of the enclosing section

[Scott Morrison]

We really should remove axiom and constant. :-)

[Scott Morrison]

Or at least attach warning lights to them. :-)

[Michael Beeson]

I'm never using 'constant' in files I intend to keep more than 15 minutes.

[Mario Carneiro]

There is a good reason for axiom and constant to exist

[Scott Morrison]

I appreciate their uses --- just we seem to see lots of people learning Lean using them in unusual ways.

[Michael Beeson]

Well, I learned of their existence by reading Theorem Proving in Lean, not by reading source files.

[Mario Carneiro]

I don't know how we could make them easier to use correctly

[Mario Carneiro]

The usage in TPIL is also an important one, where you just want to posit some things and not worry about setting them up

[Michael Beeson]

Exactly, that's what I'm doing here.

[Mario Carneiro]

but you can usually get the equivalent by replacing constant foo : type with def foo : type := sorry

[Mario Carneiro]

and that at least gives you a nice warning that you are cheating

[Mario Carneiro]

In your example file, I could see the things at the top of the file being constants and axioms, but the stuff at the bottom should definitely be variables

[Michael Beeson]

Mario, you said that my constant declaration produces a proof of a universally quantified formula. That accounts for the x y in the
next line and the M comes from the implicit parameter in the variable declaration.

[Mario Carneiro]

If you are using a one letter name, that's a strong indication that you want a variable, because constants go into the global namespace

[Mario Carneiro]

all constant, axiom, def, theorem declarations go into the global environment, and there is no local context there. So you have to universally quantify, nothing else would make sense

[Michael Beeson]

The stuff at the bottom is intended to last 15 minutes only so it doesn't matter. And now that you've explained that
my constant h produces a proof of a universally quantified formula, I understand the output. And the only thing yet to do
is look at the source code that accomplishes that.

[Mario Carneiro]

just replace constant with variable and everything else should work

[Mario Carneiro]

and also h M x y with h

[Michael Beeson]

Regarding the stuff "at the top" of the file, there was yesterday a lot of discussion about how to formalize a first-order theory
in lean. Plan A: constants and axioms. Plan B: use a structure. Plan C: use a class. So this code is using Plan C. And I also
implemented Plan A.

[Michael Beeson]

Yes, I already tried replacing constant with variable and saw that it does work. So thank you (and the rest of you) for
explaining this. I guess I have this straight now.

[Mario Carneiro]

For an industrial strength implementation, something that is going into mathlib, you should use plan B or plan C. But for your own file plan A is probably easier

[Mario Carneiro]

in this particular case I think plan C is good because it will give you access to all the notations without much difficulty

[Mario Carneiro]

You could look at set_theory.zfc for inspiration on setting up set theory

[Michael Beeson]

In the following code, the inference by eq.subst in the last line fails, though its arguments are as desired as shown by the
preceding #check commands. I know the reason for this failure but not the cure. The reason is that eq.subst takes two
arguments, the first an equality x= y and the second of the form P x, and produces P y. The elaborator uses higher-order unification to synthesize the appropriate P in case the second argument doesn't already have the form of an application to x. In the example at hand, it has to synthesize P = \lambda z. x \in z, which is too much for it to manage. That is the interpretation of the error you get, which ends up with "but the expected type must be shown". Can anyone tell me how to fix this?

set_option default_priority 100
reserve infix ` ∈ ` : 49
class  Model (M:Type)  :=
(mem : M → M → Prop)
(pair: M → M → M)
(single: M → M)
(infix  ∈  :=  mem )
(notation `{` a `,` b `}` := pair a b)
(extensionality_axiom:  ∀ a b, (∀ x, (mem x a ↔ mem x b)) → a=b)
(pairing_axiom:  ∀ x a b, (x ∈ {a,b} ↔ (x = a ∨  x = b)))
( single_definition : ∀ x, single x = {x,x})
(notation `{` a `,` b `}` := pair a b)

open Model
infix  ∈ :=  mem
notation `{` a `,` b `}` := pair a b
variables (M:Type) [Model M] (a b x y z u v w X R W: M)

#check eq.symm(single_definition x)


lemma single_definition_reverse : ∀ x:M, {x,x}  = single x :=
   λ x, eq.symm(single_definition x)


 variable h:x=y

 #check  (pairing_axiom x y y).2 (or.inl h) /- x ∈ {y,y} -/
 #check  (single_definition_reverse M y )   /- {y,y} = single y -/

 #check eq.subst  (single_definition_reverse M y )
            ((pairing_axiom x y y).2 (or.inl h))
            /- expecting x ∈ single y  but get error -/

[Andrew Ashworth]

Well, higher order unification is difficult. When it fails, you may need to explicitly provide the motive with the @ annotation

[Patrick Massot]

What are you trying to achieve with all those eq.subst? I've been using Lean for more than two years and I've written eq.subst anywhere.

[Patrick Massot]

It looks very much like you're going against the flow of Lean.

[Andrew Ashworth]

He is doing exercises to learn Lean

[Patrick Massot]

I understand this. But they look like very weird exercises.

[Patrick Massot]

Fighting Lean instead of letting it work for you.

[Andrew Ashworth]

He is a logician doing logic? Such a person might be more concerned with the foundations than others in this chat :upside_down:

[Michael Beeson]

I have x \in {y,y} and I have {y,y} = single y, and I want to conclude x \in single y.
I do not see any reason to consider that a "weird" exercise. Just answer the question, if you can, please, no need to comment on
whether you like the question or not.

[Andrew Ashworth]

Anyway, it is often the case that you need to help Lean unify things. This is discussed further in 6.10 of TPIL. You can go a long way with judicious use of the @ operator and explicit expected type annotations using the : operator.

[Patrick Massot]

example : x ∈ {y,y} → x ∈ single y :=
by { intro, rwa single_definition y }

See? If you explain what you want to achieve then people can help you, even if you don't like reading comments.

[Michael Beeson]

My aim is not just to prove that little fact. My aim is to understand how Lean works. The tactic rwa has a very complicated definition.
I did not know about rwa and I'm grateful to learn about it. But my aim here is not just to get Lean to say some proof is correct. I am trying to understand how Lean works. eq.subst is no doubt important to rewrite_cfg which occurs in the first line of the definition of rwa.
It is bound to be the "guts" of equality reasoning. That simple first-order equality reasoning requires higher-order unification that sometimes fails, even on very simple examples, is interesting and not very wonderful.

[Michael Beeson]

But you DID give me a way to prove that example, and again, thank you for that.
Andrew, can it be done with @ as well, without using a complicated tactic?

[Koundinya Vajjha]

You can try: #check @eq.subst _ _ _ _ (single_definition_reverse M y ) ((pairing_axiom x y y).2 (or.inl h))

[Andrew Ashworth]

Higher order unification not being very wonderful in Lean 3 was a deliberate design choice. There was a lot more effort put into heuristics for solving it in Lean 2, but it was impossible to figure out why things wouldn't unify. So it is much dumber, but easier to reason about in Lean 3. The time it takes to do unification is also much lower; which is actually something people worry about when reasoning about large proofs.

[Michael Beeson]

It seems from the penultimate paragraph of 6.11 in TPIL, that the attribute of eq.subst itself is what is important here,
and it is set to [elab_as_eliminator], which apparently tells it to turn on higher-order unification. I guess if you put @ in front of the call you are indicating that you are going to provide some types yourself. No examples are given in TPIL 6.11 of how to do that.

[Andrew Ashworth]

I think it's first introduced in section 2.9

[Michael Beeson]

Ah, at the end of 2.9 is the definition of @. So @eq.subst is eq.subst with all arguments required explicitly.
And you can see from #check @eq.subst what the implicit arguments are. And #check @@eq.subst only makes
some of the implicit arguments be required. So I'm beginning to see how this works.

[Michael Beeson]

Thank you for pointing me to the end of 2.9.

[Michael Beeson]

You are not providing "types". You are providing formerly-implicit arguments. The text in section 6.11 could be clarified and
a pointer to 2.9 would be nice.

[Michael Beeson]

So then somewhere in the guts of rwa, there is a workaround for this problem. I'm guessing that higher-order unification
is abandoned and some good old-fashioned substitution is used.

[Michael Beeson]

After all rewrite technology long predates higher-order unification and is much, much more efficient.

[Patrick Massot]

The answer is probably in https://github.com/leanprover-community/lean/blob/2414e7acd83fd7699966ac19aacb4755ce9d5332/src/library/tactic/rewrite_tactic.cpp#L32-L101

[Andrew Ashworth]

doesn't it look so much nicer in Lean 4? https://github.com/leanprover/lean4/blob/dd4fac2a7b337d75ddfcd42cc1bf02d2b3219a1d/src/Init/Lean/Meta/Tactic/Rewrite.lean

[Andrew Ashworth]

Probably not :grinning_face_with_smiling_eyes:

[Mario Carneiro]

@Michael Beeson The major downside of proving lemmas with #check like this is that you haven't provided the expected type. This is crucial for the elab_as_eliminator elaboration method used for functions like eq.subst. You should use example or theorem to state your goals, then provide proofs of them, rather than using #check. Or if you must use #check, use #check (term : type) instead of just #check term.

[Mario Carneiro]

Michael Beeson said:

After all rewrite technology long predates higher-order unification and is much, much more efficient.

Lean doesn't actually do higher order unification in the sense used in this sentence. The elab_as_eliminator method solves higher order unification problems using essentially a rewrite: When matching P t against the goal |- g, it finds all occurrences of t in g, replaces them with x, and P becomes \lam x, of the result.

[Mario Carneiro]

this is obviously not complete as a proof procedure but it is an easy heuristic to understand

[Michael Beeson]

If anyone cares, here's the way to make eq.subst work correctly using @@. What I learned from this:
How @ and @@ work; that first-order equality reasoning with eq.subst requires using @@ and helping out
the higher-order unification by hand; hence rwa is sometimes better; perhaps (probably) rwa doesn't use
higher-order unification at all. What I have yet to learn: why eq.subst DOES work in some algebraic examples
I saw in TPIL, and why they are easier than this apparently mindlessly simple example that doesn't work without using @@.

set_option default_priority 100
reserve infix ` ∈ ` : 49
class  Model (M:Type)  :=
(mem : M → M → Prop)
(pair: M → M → M)
(single: M → M)
(infix  ∈  :=  mem )
(notation `{` a `,` b `}` := pair a b)
(extensionality_axiom:  ∀ a b, (∀ x, (mem x a ↔ mem x b)) → a=b)
(pairing_axiom:  ∀ x a b, (x ∈ {a,b} ↔ (x = a ∨  x = b)))
( single_definition : ∀ x, single x = {x,x})
(notation `{` a `,` b `}` := pair a b)

open Model
infix  ∈ :=  mem
notation `{` a `,` b `}` := pair a b
variables (M:Type) [Model M] (a b x y z u v w X R W: M)

#check eq.symm(single_definition x)


lemma single_definition_reverse : ∀ x:M, {x,x}  = single x :=
   λ x, eq.symm(single_definition x)


 variable h:x=y

 #check h
 #check nat

 #check  (pairing_axiom x y y).2 (or.inl h) /- x ∈ {y,y} -/
 #check  (single_definition_reverse M y )   /- {y,y} = single y -/

 example: x ∈ {y,y} → x ∈ single y := by {intro, rwa single_definition y}

 #check eq.subst
 #check @@eq.subst

  #check @@eq.subst (λ z, x ∈ z) (single_definition_reverse M y )
            ((pairing_axiom x y y).2 (or.inl h))

[Mario Carneiro]

that first-order equality reasoning with eq.subst requires using @@ and helping out the higher-order unification by hand

This is not true. As I said above, what it requires is the expected type, which is almost always available when you use lean the way it is expecting you to

[Mario Carneiro]

Lean's elaboration works from the outside in. It is important to understand this if you want to understand how to predict elaboration errors

[Patrick Massot]

Mario, could you elaborate on this latest message?

[Patrick Massot]

Maybe with some tricky example?

[Kenny Lau]

if you write (a : A) = (b : B), Lean will try to coerce b to have type A

[Kenny Lau]

Lean elaborates from left to right

[Patrick Massot]

I understand left to right. Mario wrote "from the outside in".

[Mario Carneiro]

The coercion arrows in (n + n : int) where n : nat go as \u n + \u n because lean is working from the outside in, it delays the coercion until it can't do anything else

[Patrick Massot]

I sort of know that, because it's useful to debug coercion issues. But I'd like to know more

[Kenny Lau]

"left to right" is just "outside in" for prefix notation

[Mario Carneiro]

There are more extreme examples where elaboration literally just stops because it did things in the wrong order

[Mario Carneiro]

You could say left to right and outside in

[Mario Carneiro]

or "prefix traversal" of the term if you know about that

[Mario Carneiro]

example := ∀ n, (n:ℕ) + n = n.succ -- works
example := ∀ n, n.succ = (n:ℕ) + n -- fails
example := ∀ n, (n:ℕ) + n.succ = n -- works
example := ∀ n, n.succ + (n:ℕ) = n -- fails
example := ∀ n, (n.succ:ℕ) + n = n -- fails
example := ∀ n, (n:ℕ).succ + n = n -- works

To determine which of these will work, you have to know that n.succ fails immediately if the type of n is not yet known, and the elaboration proceeds in prefix order trying to assign types to all the subterms

[Patrick Massot]

The only difficult one for me is example := ∀ n, (n.succ:ℕ) + n = n -- fails

[Mario Carneiro]

There, you know that n.succ, whatever it is, has type nat, but you still don't know what type n has

[Patrick Massot]

It looks to me the type ascription is outside the n.succ so it should come first

[Mario Carneiro]

it does

[Mario Carneiro]

but it's not good enough because it might be T.succ : T -> nat and n has type T

[Patrick Massot]

I see

[Mario Carneiro]

the reason dot notation fails immediately is that if the type isn't figured out right now, we don't even know what function we are applying so type inference fails utterly

[Patrick Massot]

Makes sense

[Mario Carneiro]

It could probably be improved a bit if it holds off on elaborating this subtree and finishes up the other siblings before trying again; that would eliminate the left-right dependence

[Michael Beeson]

(deleted)

[Michael Beeson]

variables (x y :nat)
constant f: nat->nat->Prop
#check (λ z, f x z)y

I expected to get f x y, but instead I get back the unreduced term.
Why?

[Mario Carneiro]

#check doesn't reduce anything, it just typechecks the term

[Mario Carneiro]

use #reduce for this

[Mario Carneiro]

be warned that #reduce fails on most nontrivial examples

[Mario Carneiro]

also you are mixing variable and constant again

[Mario Carneiro]

the same example works with everything a variable

[Michael Beeson]

#reduce works on this example. So what can I put in my code to get that done, as opposed to at the command level?

[Mario Carneiro]

you don't have to write anything, reduction happens automatically as necessary

[Michael Beeson]

Sorry about variables and constants, but I'm not even saving this file.
Well, reduction doesn't seem to happen automatically in my code...

[Mario Carneiro]

do you have any target theorem?

[Mario Carneiro]

I'm not sure what saving the file has to do with anything

[Mario Carneiro]

I'm saying that variable is better suited for short lived terms

[Mario Carneiro]

reduction happens when it is forced to happen

[Mario Carneiro]

but doing reduction eagerly would be a very bad idea

[Michael Beeson]

OK I got the point about variables, I'll try to do better in the future.

[Mario Carneiro]

because most definitions are sitting on a huge stack of other definitions such that a full reduction would result in an astronomically large term

[Mario Carneiro]

this is why #reduce fails

[Mario Carneiro]

so instead reduction is performed only when there is a type mismatch in an application

[Mario Carneiro]

and only enough to resolve the difference

[Mario Carneiro]

for an example using #check, consider #check (rfl : (λ z, f x z)y = f x y)

[Mario Carneiro]

since rfl is a proof of a = a, lean has to reduce the lhs until it matches the rhs in order to agree that this is type correct

[Michael Beeson]

TPIL says that attributes are applied to definitions in order to solve this problem.

[Mario Carneiro]

what problem?

[Mario Carneiro]

The @[reducible] attribute can be applied to a definition as a hint for certain tactics to unfold more definitions than they normally would during unification, but they still don't reduce unless they need to