dep hd

Stream: general

[Thorsten Altenkirch]

I am just trying to prove infectivity of :: directly (I know I can use injection). But lean doesn't like my dependent hd. Maybe I am overlooking something obvious?

def Hd : list A → Type
| [] := unit
| (a :: l) := A

def hd : Π l : list A , (Hd l)
| hd [] := unit.star
| hd (a :: l) := a

[Anne Baanen]

This works for me:

variables {A : Type}

def Hd : list A → Type
| [] := unit
| (a :: l) := A

def hd : Π l : list A , (Hd l)
| [] := unit.star
| (a :: l) := a

[Anne Baanen]

Why the equation compiler decides to give a "syntax error" instead of saying there are too many arguments I don't know.

[Thorsten Altenkirch]

Ah stupid me. I always forget that lean doesn't repeat the function name like most functional languages.

[Kevin Buzzard]

@Thorsten Altenkirch in private correspondence you have indicated to me that you don't like the syntax of Lean 3's equation compiler, and you showed me examples of syntax in other languages which you said were "more modern". You know we have a #lean4 stream now lean 4 has been released. I wonder whether the more powerful elaborator of lean 4 would be more to your taste, and I think that right now might be a really good time to have a discussion about how far things can be pushed -- the lean 4 devs are watching that stream and seem to me to be very receptive to new ideas right now. Maybe you should post some of your comments about the lean 3 equation compiler there and ask if the things you're looking for are in lean 4?

[Thorsten Altenkirch]

Now I have another problem when trying to use hd to prove infectivity:

def Hd : list A → Type
| [] := unit
| (a :: l) := A

def hd : Π l : list A , (Hd l)
| [] := unit.star
| (a :: l) := a


theorem inj_hd : ∀ (a a':A)(l l' : list A), a :: l = a' :: l' → a = a' :=
begin
  assume a a' l l' h,
  change hd (a :: l) = (hd (a' :: l')),

It says unexpected argument at application hd (a' :: l') and that it would expect a::l ???

[Thorsten Altenkirch]

Kevin Buzzard said:

Thorsten Altenkirch in private correspondence you have indicated to me that you don't like the syntax of Lean 3's equation compiler, and you showed me examples of syntax in other languages which you said were "more modern". You know we have a #lean4 stream now lean 4 has been released. I wonder whether the more powerful elaborator of lean 4 would be more to your taste, and I think that right now might be a really good time to have a discussion about how far things can be pushed -- the lean 4 devs are watching that stream and seem to me to be very receptive to new ideas right now. Maybe you should post some of your comments about the lean 3 equation compiler there and ask if the things you're looking for are in lean 4?

I can do but my impression was that people in the lean community got used to the syntax (which actually originates from coq).

[Kevin Buzzard]

Lean 4 has a super-powerful macro system so what I am really interested in is whether the features you wanted can be emulated by these macros. It would be a good test for the system.

[Kevin Buzzard]

People like you who have experience with multiple provers and languages can bring new ideas to Lean and what I'm saying is that right now is a good time to bring those ideas.

[Kevin Buzzard]

So far I have been really impressed with what can be done. For example lean 3 has a calc environment and it's not in lean 4 but when someone mentioned this, someone else just knocked up a macro to emulate it.

[Kevin Buzzard]

All this is happening in #lean4

[Reid Barton]

Thorsten Altenkirch said:

Now I have another problem when trying to use hd to prove injectivity:

def Hd : list A → Type
| [] := unit
| (a :: l) := A

def hd : Π l : list A , (Hd l)
| [] := unit.star
| (a :: l) := a


theorem inj_hd : ∀ (a a':A)(l l' : list A), a :: l = a' :: l' → a = a' :=
begin
  assume a a' l l' h,
  change hd (a :: l) = (hd (a' :: l')),

It says unexpected argument at application hd (a' :: l') and that it would expect a::l ???

The default elaboration strategy is outside-in and expects the type of the right-hand side to be Hd (a :: l) and doesn't consider that this might be the case even if the argument is not a :: l. You can force it to elaborate inside-out by inserting a : _ inside those handy extra parentheses on the right-hand side.