James Gallicchio

Stream: new members

[James Gallicchio]

Hi everybody! I'm a CS student at Carnegie Mellon, interested in formal verification and programming languages generally :)

I've been writing a formalization of super basic register machines in Lean to learn the language. Starting to get to the point in that project where I should probably reach out here for help... so here I am!

[James Gallicchio]

Hm, so I've written a lemma which takes a couple values
{ip : fin ic} {regs : vector ℕ rc}
and then is stated in terms of the object
{ip := some ip, regs := regs} : state ic rc
(note the some ip rather than ip)

When trying to use this lemma, I have an expression step M c.s : state ic rc and a hypothesis that (step M c.s).ip = some ip; how would I then apply the lemma?

[James Gallicchio]

(if this seems to indicate a fundamental issue with how I'm representing the problem, that'd also be appreciated, haha! not sure if the issue is with how I wrote out the hypotheses of the lemma or the application of the lemma or with the representation altogether)

[Bryan Gin-ge Chen]

Can you share a #mwe ?

[James Gallicchio]

https://gist.github.com/JamesGallicchio/87e40a3fbd0b4c7ab3c1063f558517ad something like this -- I know in this mwe I can just use the definition of pred_a, but suppose the lemma is much less trivial than this and I want to use the lemma here instead

[James Gallicchio]

For the full context not mwe, this is the sorry I'm trying to fill
https://github.com/JamesGallicchio/lean_rms/blob/master/src/register_machine.lean#L229

[James Gallicchio]

oh, wait, in that mwe a simple rewrite works for applying the lemma

[Scott Morrison]

(#mwe's that fit inside a code block here are way more likely to get help; also the process of minimising often reveals the solution!)

[James Gallicchio]

Okay, I reorganized a bunch and think I have a better MWE:

structure mystruct := {a : ℕ} {b : ℕ}

theorem mytheorem (s : mystruct)
  : s = {a := s.a, b := s.b}
  := sorry

Not sure how to fill this sorry..?

[James Gallicchio]

Wait, cases splits up the structure into its projections? :joy: cases seems to do so much (I tried it randomly!)

[Eric Wieser]

by cases s; refl

[James Gallicchio]

So the reason cases works there is because structures are just inductive types with a single constructor; cases makes a case for that one constructor and introduces all the arguments. Right?

[James Gallicchio]

Hm, how do you prove to the typechecker that certain types are equivalent?

def test : vector ℕ ic := vector.of_fn (λ _, 0)
def thing : vector ℕ (1+ic) := vector.append ⟨[0],rfl⟩ test

Say I wanted thing : vector ℕ ic.succ instead.

[James Gallicchio]

I'm sure this has to do with my fundamentally not understanding how equality works in Lean, so any resources/pointers there would be super appreciated!

[James Gallicchio]

(Starting off by reading the equality section of TPIL, hopefully my answer lies in there...)

[Yakov Pechersky]

To prove two types are equivalent, you need to provide an explicit iso between them. To start, here is an example:

import data.vector2

variable (ic : nat)

def test : vector ℕ ic := vector.of_fn (λ _, 0)
def thing : vector ℕ (1+ic) := vector.append ⟨[0],rfl⟩ (test ic)

def thing2 : vector nat ic.succ := cast (by rw add_comm) (thing ic)

[Yakov Pechersky]

In fact, you can use equiv.cast to get the iso

[Yakov Pechersky]

def thing3 : vector nat ic.succ := equiv.cast (by rw add_comm) (thing ic)

[James Gallicchio]

Ahh, cast is exactly what I needed. Thank you!

[Yakov Pechersky]

But careful, it is difficult to make proofs about structures/terms that have been constructured through complex cast manipulation

[James Gallicchio]

Hm... so my goal should be to avoid whenever possible?

[Yakov Pechersky]

In what contexts do you need to modify types likes this? It's fine to do so if you know what you're striving for. What's your use case?

[James Gallicchio]

Ended up rewriting a bunch of stuff to work around casts (so far :rolling_on_the_floor_laughing:)

[James Gallicchio]

It was a good indication that something in my design wasn't great. Hopefully we're out of the swamp there

[James Gallicchio]

But now I am stuck wondering how this definition works:
https://leanprover-community.github.io/mathlib_docs/computability/primrec.html#primcodable
In my head, the prim type shouldn't typecheck.
encodable.decode α n : option ℕ, but encodable.encode : ℕ → ℕ... how the heck?

[Mario Carneiro]

It's playing a bit of a trick. The type of encodable.encode isn't ℕ → ℕ, it's α → ℕ (for all encodable α), and there is an instance saying option α is encodable if α is, so it is using the decode instance for α and applying the encode instance for option α to the result.

[James Gallicchio]

Ahh, that makes sense

[James Gallicchio]

I guess I have a bit of a general question about choosing representations -- in doing some indexing trickery, I'm struggling to pick between representing a certain index as fin n.succ or option (fin n), where none would correspond with fin.last n

Sometimes the fin n.succ representation is super elegant, but other times it's easier to just case on an option (fin n)... is there an easy way to case on whether i : fin n.succ is fin.last n or else equals i' : fin n?

(If not, I'm gonna go with the option (fin n) one since it's pretty straightforward going to the fin n.succ representation from there)

[Eric Rodriguez]

option (fin n) is good, but I think the vector methods like docs#fin.cons will work best (and yes, this appends at 0 instead of at n: this is honestly so much easier to work with in Lean)

[Eric Rodriguez]

if you wanna append at the end, there's docs#fin.snoc (cons backwards). i would strongly advise you to avoid this unless it's needed

[James Gallicchio]

hmm, yeah. Lean _really_ doesn't like working at the end of the range. gonna just go with option (fin n)

[Yakov Pechersky]

There are also docs#fin_succ_equiv and docs#fin_succ_equiv' to easily convert between the two options you said

[Yakov Pechersky]

Where fin_succ_equiv sends 0 to none, and the fin_succ_equiv' version lets you specify the "hole" explicitly.

[James Gallicchio]

I was looking through the fin-tuple stuff -- is there a reason why both the fin tuples are defined and vector? Or rather where should I prefer one over the other? I just used vector cuz it was what I found first

[Yakov Pechersky]

Depends on your use case. Of course, there are explicit equivs between all of these. But the API is different, and there might be different computability aspects

[James Gallicchio]

vector has treated me well so far, so I'll stick with it :thumbs_up: I did need a couple more quick vector lemmas that aren't in mathlib yet, but I assume the lemmas accumulate from people finding new use cases :-)

[Mario Carneiro]

fin tuples are generally easier to use for mathematics and have a better API

[Adam Topaz]

fin tuples can be heterogeneous as well, IIRC

[James Gallicchio]

Yeah; I kinda assumed that vectors would just have a better API for homogeneous tuples but maybe not :joy: I'm gonna ask for feedback on my code once it's in a better state and maybe then I'll review whether I chose the wrong API :p

[James Gallicchio]

(I'm mostly just using the nth and update_nth functions, along with lemmas like vector.nth_update_nth_same. not sure how i'd do that with the fin tuples)

[Yakov Pechersky]

You could use docs#function.update, with help from lemmas like docs#fin.cons_update

[James Gallicchio]

Hi, back to working on this project :) is it at all possible to do something like

match i with
| 0 := ...
| 1 := ...
end

for i : fin 2 or similar? I see the fin2 type which might be helpful here since it's defined inductively?

[Eric Wieser]

Yes, but with ⟨0, _⟩ instead of 0 etc

[Eric Wieser]

Although often ![..., ...] is a better way to define such a function

[James Gallicchio]

hm, is that ![] syntax behind some import?

[James Gallicchio]

The exhaustiveness checker does not like ⟨0, _⟩ :/ I assume I'd need to have an extra case like ⟨n,h⟩ that derives bottom or something if I wanted the compiler to not complain

[Ruben Van de Velde]

Notation is here: https://leanprover-community.github.io/mathlib_docs/data/matrix/notation.html

[James Gallicchio]

Oh, huh! Yeah, this could work. I'm a bit sad that the pattern match doesn't directly work, because in this context it actually is much more readable if each item is numbered...

[Yakov Pechersky]

I think Anne did add support for the equation compiler to do what you'd like here, via wf recursion

[Yakov Pechersky]

docs#fin.has_well_founded. So it's like what Eric said

[Eric Wieser]

That instance is only needed if you actually need to recurse. If you're just case matching the equation compiler doesn't need it

[James Gallicchio]

:thinking:

λ (i : fin 1), match i with
⟨0,_⟩ := instr.dec (r_map r) (some (ai_map 0)) none
end

The compiler complains about missing the case

rst._match_1 r _x _x_1 r_map ai_map ⟨nat.succ _, _⟩

which is the absurd case. I can get around it by adding

λ (i : fin 1), match i with
| ⟨0,_⟩ := instr.dec (r_map r) (some (ai_map 0)) none
| ⟨n+1,hi⟩ := begin simp at hi, exact hi.rec_on _ end
end)

(not sure if there's a more canonical way to use absurdity)
This is a bit unsatisfying though, and also won't be very practical if the case is n.succ.succ.succ.succ.succ.succ unless there's a better way to do it in that case.

[Sebastien Gouezel]

#mwe is always a good idea :-)

[James Gallicchio]

ah, ye, I can strip this down, gimme a sec

[Kevin Buzzard]

We're hoping you can just give us something which compiles for us :-) (but in general your strategy of using false.elim for the cases which can't happen is the correct one, if you can't persuade the equation compiler to do it for you)

[James Gallicchio]

def mwe : fin 2 → string := λ i, match i with
| ⟨0,_⟩ := "zero!"
| ⟨1,_⟩ := "one!"
| ⟨2,_⟩ := "two!"
| ⟨n+3,hi⟩ := /- some way to absurdity -/
end

This doesn't quite compile, but gives the idea

[Kevin Buzzard]

You can use sorry to make it compile. Using the rcases? tactic you can prove it like this:

import tactic

def mwe : fin 2 → string := λ i, match i with
| ⟨0,_⟩ := "zero!"
| ⟨1,_⟩ := "one!"
| ⟨2,_⟩ := "two!"
| ⟨n+3,hi⟩ := false.elim (by rcases hi with _ | ⟨_, _ | ⟨_, ⟨⟩⟩⟩)
end

[James Gallicchio]

Haven't heard of rcases (and don't understand how it works :joy: will look at that) but I think this pattern grows with the size of the constant, no? I don't plan to have particularly large constants but it's still not ideal to have to expand that each time

[Kevin Buzzard]

I'm abusing the definition of <, which is defined as an inductive type. rcases is just recursive cases, available in the mathlib repo. The pattern grows with the size of the constant, as does your code dealing with the valid cases.

[Horatiu Cheval]

The case of 2 is also absurd here, right? fin 2 is just 0 and 1, isn't it? (I have never really worked with fin)

[Yakov Pechersky]

import tactic

def mwe : fin 2 → string
| ⟨0,_⟩ := "zero!"
| ⟨1,_⟩ := "one!"
| ⟨n+2, hi⟩ := absurd
  (show (2 < 2), from ((nat.le_add_left 2 n).trans_lt hi))
  (lt_irrefl _)

[Kevin Buzzard]

this is better than my solution because it doesn't increase linearly as the number gets bigger

[Yakov Pechersky]

Also this generates better definitional things because it's not hidden behind a match

[Ruben Van de Velde]

Slightly shorter with false.elim:

import tactic

def mwe : fin 2 → string
| ⟨0,_⟩ := "zero!"
| ⟨1,_⟩ := "one!"
| ⟨n+2, hi⟩ := (lt_irrefl _ $ (nat.le_add_left 2 n).trans_lt hi).elim

[James Gallicchio]

Yakov Pechersky said:

Also this generates better definitional things because it's not hidden behind a match

Is there a way to do that for anonymous function declarations?

[Yakov Pechersky]

For fin? I would just do matrix notation:

import tactic
import data.matrix.notation

def mwe : fin 2 → string
| ⟨0,_⟩ := "zero!"
| ⟨1,_⟩ := "one!"
| ⟨n+2, hi⟩ := absurd
  (show (2 < 2), from ((nat.le_add_left 2 n).trans_lt hi))
  (lt_irrefl _)

def mwe' : fin 2 → string :=
!["zero!", "one!"]

example : mwe = mwe' :=
begin
  ext i,
  fin_cases i;
  refl
end

[James Gallicchio]

Yeah... :/ The reason I was preferring the explicit match syntax is because I'm trying to replicate a syntax that is like

1: line of code
2: line of code
3: line of code

where the lines make reference to each other. so it's helpful to have the line numbers on the side as part of the syntax (since that makes it easy to see what line 3 is, for instance). But I may just revert back to matrix notation.

[Yakov Pechersky]

You can't do self-referential definitions that rely on match.

[Yakov Pechersky]

import tactic
import data.matrix.notation

def mwe : fin 5 → string
| ⟨0,_⟩ := "zero!"
| ⟨n+1, hi⟩ := mwe ⟨n, (nat.le_add_right _ _).trans_lt hi⟩

def mwe' : fin 5 → string := λ i, match i with
| ⟨0,_⟩ := "zero!"
| ⟨n+1, hi⟩ := mwe' ⟨n, (nat.le_add_right _ _).trans_lt hi⟩ -- doesn't know about mwe'
end

[Yakov Pechersky]

Because lean needs to know that the function terminates. The equation compiler can figure that out, either by structural or well-founded recursion. That isn't available in match.

def mweN : ℕ → string
| 0 := "zero!"
| (n+1) := mweN n

def mweN' : ℕ → string := λ i, match i with
| 0 := "zero!"
| (n+1) := mweN' n -- still doesn't know
end

[James Gallicchio]

Yeah -- I don't mean literal self reference, just that when you say 3 in the "code" part it refers to line 3 of the "program," so it's helpful for line 3 to be labelled with a 3. I could get what I want via the matrix notation and comments:

![
/- 1: -/ ...,
/- 2: -/ ...,
/- 3: -/ ...
]

which is what I think I'll end up doing.

[Yakov Pechersky]

fyi, match and eq compiler does not need to have the cases in "order" -- how could it for types that have no inherent order for the terms?

import tactic
import data.matrix.notation

def mwe : fin 5 → string
| ⟨n+1, hi⟩ := mwe ⟨n, (nat.le_add_right _ _).trans_lt hi⟩
| ⟨0,_⟩ := "zero!"

[Eric Wieser]

by linarith is able to close the absurd goal too, which while slower is easier to dismiss

[James Gallicchio]

Lots more progress on this :) I'm finally hitting the wall of stuff I don't know again, though. Weird issue:

example (n : ℕ) : ![0,n,n] = λ r : fin 3,
  @sum.cases_on _ _ (λ _, ℕ) (![sum.inl 1, sum.inl 0, sum.inr n] r) ![n, 0] (λ x, x)
  := begin
    ext,
    fin_cases x,
    iterate { admit, },
  end

I'm trying to prove some small fin tuples equal, but for some reason simplifying these cases does not fully evaluate...

[James Gallicchio]

Using simp on the first case reduces it to

0 = sum.rec ![n, 0] (λ (val : ℕ), val) (![sum.inl 1, sum.inl 0, sum.inr n] 0)

which is clearly still simplifiable. Not sure why it's having a hard time reducing that.

[Mario Carneiro]

Raw sum.rec can block computation, because it is a dependent function. You should avoid using it and use match or definitions by the equation compiler instead

[Mario Carneiro]

using sum.elim also works

example (n : ℕ) : ![0,n,n] = λ r : fin 3,
  sum.elim ![n, 0] (λ x, x) (![sum.inl 1, sum.inl 0, sum.inr n] r) :=
begin
  ext,
  fin_cases x; simp,
end

[James Gallicchio]

Ah, okay, will give that a shot!

[James Gallicchio]

Another weird thing, getting this error

rewrite tactic failed, motive is not type correct
  λ (_a : ℕ), init (ic1.succ + ic2) = some (⇑(fin.cast_add ic2) 0) = (init _a = some (⇑(fin.cast_add ic2) 0))

MWE:

import data.fintype.fin

@[simp] def init (ic : ℕ) : option (fin ic)
  := match ic with 0 := none | icp+1 := some 0 end

@[simp] def map_i (ic1 ic2 : ℕ) (i : fin ic1) : fin (ic1+ic2)
  := fin.cast_add ic2 i

example (ic1 ic2 : ℕ) : init (ic1.succ + ic2) = some (fin.cast_add ic2 0)
  := begin
    conv {
      to_lhs,
      rw nat.add_comm,
    },
    sorry,
  end

Never seen that error before, poked around on zulip and Mario had suggested using conv, but I played around and couldn't figure how to avoid it...

[Scott Morrison]

So the problem is that when you are trying to change ic1.succ + ic2 into ic2 + ic1.succ, you would at the same time need to change the types of both sides of equation!

[Scott Morrison]

This is avoiding the question, perhaps, but you could use:

import data.fintype.fin

def init : Π n, option (fin n)
| 0 := none
| (n+1) := some 0

example (n m : ℕ) : init (n.succ + m) = some (fin.cast_add m 0) :=
by induction m; refl

[Scott Morrison]

(Asides: I'm not sure why you put @[simp] on both of your definitions. This was probably unnecessary. Also map_i is not needed for a MWE.)

[James Gallicchio]

(Ah, sorry, hangovers from when I was cutting it down). Is there a reason this needs to be by induction?

[Scott Morrison]

You should think a bit about this: if you could rewrite n.succ + m into m + n.succ on the LHS here, what type would you need to have on the RHS? What term would you expect to see there after the rewrite?

[James Gallicchio]

Mm, fair enough. I guess the other option would be to insert a cast there?

[James Gallicchio]

Cuz I could put a cast on both sides to option (fin (n+m).succ

[James Gallicchio]

Actually, that doesn't quite make sense either, hm