context within match expression

Stream: general

[Hans-Dieter Hiep]

Hi! I have a basic question about match expressions. It seems that part of the context is missing. Let me demonstrate by example:

def test (t : bool) : bool :=
  match t with
  | tt := let H : t = tt := begin admit end in t
  | ff := ff
  end

Here, before the admit tactic, we see as context:

t : bool,
_match : bool → bool
⊢ t = tt

But the point is that within this case, we know that t = tt, otherwise it would not be matched. How do I gain back this information? Do I need to use the recursor of bool, bool.rec?

[Hans-Dieter Hiep]

I have written this program now:

def test2 (t : bool) : bool :=
  begin
    cases H : t,
    { exact ff },
    { have : t = tt, apply H, exact t }
  end

And printed the result. It appears that printing #print test._match_1 and #print test2 reveals their difference. The match clause apparently hides this fact. By using bool.cases_on I can directly access the needed information.

[Hans-Dieter Hiep]

Somehow, I expected a similar functionality for the match clause as is provided by the cases tactic. Something like match (H : t) with, but that is not syntactically valid, nor documented. Am I missing something?

[Rob Lewis]

Another option:

def test (t : bool) : bool :=
  match _, rfl : ∀ b, t = b → _ with
  | tt, h := let H : t = tt := begin admit end in t
  | ff, h := ff
  end

[Hans-Dieter Hiep]

Thanks! That is much neater than going into proof mode!