Zulip Chat Archive

Stream: general

Topic: context within match expression


view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 15:02):

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?

view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 15:09):

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.

view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 15:10):

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?

view this post on Zulip Rob Lewis (Feb 14 2019 at 15:11):

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

view this post on Zulip Hans-Dieter Hiep (Feb 14 2019 at 15:16):

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


Last updated: May 14 2021 at 22:15 UTC