Stream: Coq users

Topic: rewriting under binder in ssreflect style rewrite.

walker (Nov 22 2022 at 13:38):

I tried under tactic but it does not seam to work,
What I am trying to to s have some predicable naive logic automation without the need for LTAC

Require Import ssreflect.
Require Import Setoid.

Axiom iff_and_iff: forall P Q,
    (P <-> Q) <-> ((P -> Q) /\ (Q -> P)).
Axiom imp_and_iff: forall P Q R,
    (P -> Q /\ R) <-> (P -> Q) /\ (P -> R).
Axiom imp_uncurry_iff: forall (P Q R: Prop ),
    (P /\ Q -> R) <-> (P -> Q -> R).
Axiom and_split_iff : forall (P Q: Prop),
    P -> (P /\ Q <-> Q).
Definition logicE := (
    iff_and_iff,
    imp_and_iff,
    imp_uncurry_iff,
    and_split_iff
).

Lemma foo P Q: P /\ Q <-> P /\ Q.
Proof.
by rewrite !logicE.
Qed.

Lemma foo' T (P Q:T -> Prop): forall x, P x /\ Q x <-> P x /\ Q x.
Proof.
Fail under !logicE. (* if only this one works!*)
setoid_rewrite iff_and_iff.
setoid_rewrite imp_and_iff.
setoid_rewrite imp_uncurry_iff.
setoid_rewrite and_split_iff;
by setoid_rewrite and_split_iff.
Qed.

What I want is the ability to construct complex rewrites like in ssreflect while being able do use them under binders like setoid_rewrite.

Kenji Maillard (Nov 22 2022 at 13:53):

I think the right way to use the under tactic is to provide an extensionality lemma as first argument. Here's what I would do in your example:

Lemma forall_ext {A} {P Q : A -> Prop} : (forall x, P x <-> Q x) -> (forall x, P x) <-> (forall x, Q x).
Proof. move=> h; split;move=> f x; apply/h; exact (f x). Qed.

Lemma foo' T (P Q:T -> Prop): forall x, P x /\ Q x <-> P x /\ Q x.
Proof.
  under forall_ext=> x do by rewrite Under_relE !logicE.
  move=> ?????; by symmetry.
Qed.

I had to use Under_relE to remove the 'Under[ ... ] notation and get Setoid rewriting to work ok which is probably not the best way to solve this. Also I don't know what's the leftover goal.

walker (Nov 22 2022 at 14:01):

yeah this doesn't looks nice, my goal was to have one universal rewrite that does everything. my other solution was to have foral_ext as part of the rewite system and another lemma that just uncurry nested foralls before.

walker (Nov 22 2022 at 14:02):

I am starting to see limitaton of this appoach in general where i need to be extremely careful not to create rewrite cycles.

Paolo Giarrusso (Nov 22 2022 at 19:07):

Yeah, you need your rules to form a terminating rewriting system

Paolo Giarrusso (Nov 22 2022 at 19:08):

*confluent as well

Paolo Giarrusso (Nov 22 2022 at 19:18):

I mention those keywords because there's literature on them :-)

Paolo Giarrusso (Nov 22 2022 at 19:24):

Among others (https://en.wikipedia.org/wiki/Knuth%E2%80%93Bendix_completion_algorithm):

The Knuth–Bendix completion algorithm (named after Donald Knuth and Peter Bendix[1]) is a semi-decision[2][3] algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it effectively solves the word problem for the specified algebra.

one can even run it by hand

Paolo Giarrusso (Nov 22 2022 at 19:25):

the only downside is that it _is_ closed world, but that can scale well enough in many scenarios

Cyril Cohen (Nov 22 2022 at 19:32):

Kenji Maillard said:

I think the right way to use the under tactic is to provide an extensionality lemma as first argument. Here's what I would do in your example:

Lemma forall_ext {A} {P Q : A -> Prop} : (forall x, P x <-> Q x) -> (forall x, P x) <-> (forall x, Q x).
Proof. move=> h; split;move=> f x; apply/h; exact (f x). Qed.

Lemma foo' T (P Q:T -> Prop): forall x, P x /\ Q x <-> P x /\ Q x.
Proof.
  under forall_ext=> x do by rewrite Under_relE !logicE.
  move=> ?????; by symmetry.
Qed.

I had to use Under_relE to remove the 'Under[ ... ] notation and get Setoid rewriting to work ok which is probably not the best way to solve this. Also I don't know what's the leftover goal.

In principle

Lemma foo' T (P Q:T -> Prop): forall x, P x /\ Q x <-> P x /\ Q x.
Proof. by under forall_ext=> x do rewrite foo. Qed.

should have worked, but Coq must be informed that the Under protecting constant commute with equivalence... but I think this was once the case but caused loops in the setoid rewriting logic program...

Paolo Giarrusso (Nov 22 2022 at 19:35):

@Cyril Cohen yeah I ended up needing https://github.com/bedrocksystems/BRiCk/blob/906c51a4bb2a5fd2eed28fb438fc4d5509d56807/theories/prelude/under_rel_proper.v, and we did not try supporting that scenario IIUC:

These instances [...] do not allow rewriting with a different relation [S] under [Under_rel T R], even when one can rewrite with [S] under [R].

Paolo Giarrusso (Nov 22 2022 at 19:36):

I had asked about this in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60Proper.20.2E.2E.2E.20.28Under_rel.20.2E.2E.2E.29.60, and it was never clear what was supposed to happen and why those instances aren't upstream

Last updated: Apr 20 2024 at 00:02 UTC