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: Oct 13 2024 at 01:02 UTC