Stream: Coq users

Topic: ✔ transport in pattern matching

Raul (Apr 02 2023 at 19:00):

I'm trying to rewrite inside a `match .. as .. return .. with`, in order to simplify an equality.

Particularly I want to simplify the following:

``````Some a =
Some
(match f (Some x) as o return (f (Some x) = o -> U) with
| Some a0 => fun=> a0
| None => fun Ho : f (Some x) = None =>
False_rect U (option_some_proof f f_wd x Ho)
end (erefl (f (Some x))))
``````

By using

``````Heq : f (Some x) = Some a
``````

The error essentially tells me that rewriting would give an ill-typed term

``````The 6th term has type "_pattern_value_ = None" which should be coercible to
"f (Some x) = None".
``````

Gaëtan Gilbert (Apr 02 2023 at 19:33):

you can define

``````Import EqNotations.

Definition option_match_some_rw {A P vSome vNone o} {x:A} (H:Some x = o)
: match o return P o with None => vNone | Some y => vSome y end  = rew [P] H in vSome x
:= match H with eq_refl => eq_refl end.
``````

then `rewrite (option_match_some (eq_sym Heq))` should produce the goal `Some a = Some ((rew [fun o => f (Some x) = o -> U] (eq_sym Heq) in (fun _ => a)) (erefl (f (Some x)))`
then rewriting with

``````Definition constant_rw T P (x y:T) (H:x=y) B b
: rew [fun z => P z -> B] H in (fun _ => b) = fun _ => b
:= match H with eq_refl => eq_refl end.
``````

should produce the goal `Some a = Some a`

when you get "rewriting would produce an ill-typed term" it often means you need to prove a generalized lemma to make progress

Notification Bot (Apr 02 2023 at 20:16):

Raul has marked this topic as resolved.

Raul (Apr 02 2023 at 20:17):

Wow, There's some real magic in that EqNotation Module!
Thx.

Last updated: Jun 25 2024 at 15:02 UTC