Stream: Coq users

Topic: ✔ A rew lemma

Ramkumar Ramachandra (Mar 01 2022 at 14:16):

Hi, I'm trying to write a simple rew lemma, but I'm stuck here (doesn't type check).

Lemma rew_closure {A B} (P : A -> Type) {f : forall x : A, B -> P x}
  {x y : A} (H : x = y):
  rew [P] H in (fun (ε : B) => f x ε) = fun (ε : B) => (rew [P] H in f x ε).

Gaëtan Gilbert (Mar 01 2022 at 14:20):

the first one should be rew [fun x => B -> P x]

Ramkumar Ramachandra (Mar 01 2022 at 14:23):

Ah yes! ... but I'm confused now, because my goal doesn't contain that expression in the rew predicate.

Ramkumar Ramachandra (Mar 01 2022 at 14:25):

/me re-checks

Ramkumar Ramachandra (Mar 01 2022 at 15:27):

Okay, I need help help again: doesn't type-check. The lemma is getting out-of-hand.

Lemma rew_closure {A} B (P: B -> A -> Type) (Q: B -> Type) {x y: A}
  {f: forall (x: A) (ε: B), P ε x} {g: B -> A} (H: x = y):
  rew [fun ε x => B -> P ε x] H in (fun (ε: B) => f ε (g ε)) =
  fun (ε: B) => rew [P] H in f ε (g ε).

Ramkumar Ramachandra (Mar 01 2022 at 15:39):

When applying the original lemma with @Gaëtan Gilbert's fix, I get Unable to unify "?M1379 x" with ... as ... contains local variables.

Ramkumar Ramachandra (Mar 01 2022 at 15:42):

x takes epsilon as an argument, so I'm trying to re-work it.

Ramkumar Ramachandra (Mar 01 2022 at 16:48):

Never mind. I'll just stick to using map_subst.

Notification Bot (Mar 01 2022 at 16:48):

Ramkumar Ramachandra has marked this topic as resolved.

Last updated: Oct 03 2023 at 19:01 UTC