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.

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.

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.

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

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

*confluent as well

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

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

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

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

@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].

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: Jul 24 2024 at 12:02 UTC