Stream: general

Topic: equation compiler

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?

Minchao Wu (Jul 24 2018 at 16:57):

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

then you can't

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

you can't.

reason?

Kenny Lau (Jul 24 2018 at 17:00):

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

Kenny Lau (Jul 24 2018 at 17:01):

also how do you use rec or cases?

Minchao Wu (Jul 24 2018 at 17:01):

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

Kenny Lau (Jul 24 2018 at 17:01):

the b is a catch-all clause

Kenny Lau (Jul 24 2018 at 17:01):

it is intended to match everything

that's true

Minchao Wu (Jul 24 2018 at 17:02):

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

Minchao Wu (Jul 24 2018 at 17:03):

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

Kenny Lau (Jul 24 2018 at 17:03):

what was your idea with rec and cases?

Minchao Wu (Jul 24 2018 at 17:04):

also how do you use rec or cases?

you just don't use match

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?

Minchao Wu (Jul 24 2018 at 17:05):

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

Minchao Wu (Jul 24 2018 at 17:05):

namely explicitly writing down all the constructors

Simon Hudon (Jul 24 2018 at 17:28):

What you could do is:

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


Kenny Lau (Jul 24 2018 at 17:28):

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

Johan Commelin (Jul 24 2018 at 17:31):

I think that you don't have to.

Johan Commelin (Jul 24 2018 at 17:31):

That is Simon's trick.

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.

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

Minchao Wu (Jul 24 2018 at 17:34):

but this trick might work

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).

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

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,
exact n },
end


(deleted)

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?

Minchao Wu (Jul 24 2018 at 17:47):

in the case of nat there is no parameters

Simon Hudon (Jul 24 2018 at 17:48):

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

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 -/ }

Minchao Wu (Jul 24 2018 at 17:59):

Very cool, it worked

Thanks!

Minchao Wu (Jul 24 2018 at 18:00):

I wasn't aware of the case tatic

Simon Hudon (Jul 24 2018 at 18:00):

The more you know :wink:

Minchao Wu (Jul 24 2018 at 18:00):

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

Nicholas Scheel (Jul 24 2018 at 23:14):

(deleted)

Last updated: May 15 2021 at 02:11 UTC