hypotheses in term and tactic mode

Stream: general

[Sorawee Porncharoenwase]

Consider:

inductive day : Type
| mon : day
| tues : day
| wed : day
| thu : day
| fri : day
| sat : day
| sun : day

def foo : day → ℕ
| day.sun := 1
| d :=
  begin
    sorry
  end

Is there a way to get the fact that d is not day.sun at sorry?

Similarly:

def foo (n : ℕ) : ℕ :=
  if n > 13 then
    begin
      sorry
    end
  else
    42

Is there a way to get the fact that n > 13 at sorry?

My workaround for both issues to to write the entire thing in the tactic mode. For the first one, I can use cases, and deal with all non day.sun with all_goals while retaining the hypothesis that d is not day.sun. For the second one, I can use by_cases to get the desired hypothesis. However, it would be nice if there is a better way to do things.

[Yakov Pechersky]

If you do if h : d = day.sun then _ else _ in the then case you should be able to use foo.no_confusion to generate whatever you need using the h hypothesis

[Yakov Pechersky]

In the def foo case, by writing if h : n > 13 then _ else 42, the dependent hypothesis h : n > 13 will be available in the then case. In the else case, you'll have the negation of that hypothesis

[Sorawee Porncharoenwase]

thanks! :)

[Yakov Pechersky]

if c then p else q statements get interpreted as ite c p q. The dependent if h : c ... instead get interpreted as dite c ....

[Sorawee Porncharoenwase]

well, that solves the second issue, but for the first one, my above example is probably too minimal. It would be very inconvenient if I can't use pattern matching, since the function is something like:

def foo : sth → ℕ
| (sth.a (a.b (b.c x))) := x
| y := -- deal with sth.a (a.c ...), sth.a (a.d ...), sth.b ..., sth.c ...
  sorry

[Mario Carneiro]

The usual workaround I use for this is to use cases and then all_goals { proof } in all the cases other than the main one. That way you have access to the fact that y is some particular constructor different from sth.a and so on

[Mario Carneiro]

the short answer is "no, lean does not provide a way to know that y is not sth.a in the wildcard case"