Zulip Chat Archive

Stream: general

Topic: equation compiler


view this post on Zulip Minchao Wu (Jul 24 2018 at 16:56):

Hi friends, is there a way to fill up this underscore?

def foo (n : nat) : nat :=
match n with
| 0     := 0
| k     := have k  0, from _,
           0
end

Usually n is of some complicated inductive types, but I really just need to handle one specific constructor. For all the other constructors the proofs are long but exactly the same.
I could use rec or cases or if then else but that would be awkward. So I am wondering how I can refer to the facts that the equation compiler knows but are not listed as hypotheses?

view this post on Zulip Kenny Lau (Jul 24 2018 at 16:56):

use k+1 instead of k

view this post on Zulip Minchao Wu (Jul 24 2018 at 16:57):

that works in the case of nat but not other complicated inductive types

view this post on Zulip Kenny Lau (Jul 24 2018 at 16:57):

then you can't

view this post on Zulip Minchao Wu (Jul 24 2018 at 16:59):

def bar : bool  
| tt     := 0
| b     := have b  tt, from _, 1

well maybe this one is a better toy example

view this post on Zulip Kenny Lau (Jul 24 2018 at 17:00):

you can't.

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:00):

reason?

view this post on Zulip Kenny Lau (Jul 24 2018 at 17:00):

in that environment you do not know that b is not tt

view this post on Zulip Kenny Lau (Jul 24 2018 at 17:01):

also how do you use rec or cases?

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:01):

but the equation compiler knows that if it's tt then the thing is not exhaustive

view this post on Zulip Kenny Lau (Jul 24 2018 at 17:01):

the b is a catch-all clause

view this post on Zulip Kenny Lau (Jul 24 2018 at 17:01):

it is intended to match everything

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:01):

that's true

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:02):

I am saying that the compiler knows that tt will never be matched by b

view this post on Zulip Kenny Lau (Jul 24 2018 at 17:02):

but that's already outside your environment

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:03):

perhaps, so I am asking if there is a clever hack

view this post on Zulip Kenny Lau (Jul 24 2018 at 17:03):

what was your idea with rec and cases?

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:04):

also how do you use rec or cases?

you just don't use match

view this post on Zulip Kenny Lau (Jul 24 2018 at 17:04):

that works in the case of nat but not other complicated inductive types

does using rec solve this problem?

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:05):

it's the same as your suggestion of using (k+1)

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:05):

namely explicitly writing down all the constructors

view this post on Zulip Simon Hudon (Jul 24 2018 at 17:28):

What you could do is:

begin
  cases n,
  case 0 :
  { /- proof -/ },
  all_goals { /- proof -/ },
end

view this post on Zulip Kenny Lau (Jul 24 2018 at 17:28):

but how are you going to prove n != 0?

view this post on Zulip Johan Commelin (Jul 24 2018 at 17:31):

I think that you don't have to.

view this post on Zulip Johan Commelin (Jul 24 2018 at 17:31):

That is Simon's trick.

view this post on Zulip Johan Commelin (Jul 24 2018 at 17:32):

You just prove it case by case, for all cases. But then, you prove all but one case with a single proof.

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:33):

I forgot to mention that foll all the other cases I need the fact that n!=0

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:34):

but this trick might work

view this post on Zulip Johan Commelin (Jul 24 2018 at 17:35):

Right, so now you somehow need to know that fact, but now it should be even true in your environment (I hope).

view this post on Zulip Simon Hudon (Jul 24 2018 at 17:35):

Off the top of my head, cases h : n will preserve the variable n and you can do your proof with subst n and contradiction

view this post on Zulip Simon Hudon (Jul 24 2018 at 17:44):

concretely, here is how I do it:

def foo (n : nat) : nat :=
begin
  cases h : n,
  case nat.zero :
  { exact 0 },
  all_goals
  { have : n  0,
    { subst n, contradiction },
    exact n },
end

view this post on Zulip Simon Hudon (Jul 24 2018 at 17:45):

(deleted)

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:47):

when you use cases 0: to handle the specific constructor, how do you supply the arguments to that constructor?

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:47):

in the case of nat there is no parameters

view this post on Zulip Simon Hudon (Jul 24 2018 at 17:48):

(note that it's case nat.zero :, no s, and full constructor name)

view this post on Zulip Simon Hudon (Jul 24 2018 at 17:48):

if we were looking at a list for instance, it would be case list.cons : x xs { /- my proof -/ }

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:59):

Very cool, it worked

view this post on Zulip Minchao Wu (Jul 24 2018 at 17:59):

Thanks!

view this post on Zulip Minchao Wu (Jul 24 2018 at 18:00):

I wasn't aware of the case tatic

view this post on Zulip Simon Hudon (Jul 24 2018 at 18:00):

The more you know :wink:

view this post on Zulip Minchao Wu (Jul 24 2018 at 18:00):

I'm going to embrace it from now on :)

view this post on Zulip Nicholas Scheel (Jul 24 2018 at 23:14):

(deleted)


Last updated: May 15 2021 at 02:11 UTC