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".
```

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

Raul has marked this topic as resolved.

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

Thx.

Last updated: Oct 04 2023 at 20:01 UTC