Hi all. I want to rewrite inside dependent pairs, as expected this doesn't work because Coq doesn't know how to abstract.

I can instead do this:

```
Lemma sig_rewrite_aux :
∀ {T A} {P : A → Prop} {x y} (p : T → A) (h : P (p x)) (e : x = y),
P (p y).
Proof.
intros T A P x y p h e. subst. auto.
Defined.
Lemma sig_rewrite :
∀ {T A} {P : A → Prop} {x y} (p : T → A) (h : P (p x)) (e : x = y),
exist _ (p x) h = exist _ (p y) (sig_rewrite_aux p h e).
Proof.
intros T A P x y p h e. subst. reflexivity.
Qed.
```

But now I don't know how to rewrite using `sig_rewrite`

without giving `p`

explicitly. Is there a way to write a tactic that would infer it?

I was thinking something like this, but this is not possible.

```
Ltac rewrite_sig e :=
lazymatch type of e with
| ?x = ?y =>
match goal with
| |- context [ exist _ ?p ?h ] =>
match p with
| context C[ x ] =>
let q := λ y, context C[y] in
rewrite (sig_rewrite q h e)
end
end
end.
```

Thanks.

you could try to `pattern`

the term `x`

to have a goal of the shape `(fun x => ... exist _ p h ...) x`

and then do a pattern matching with a second order pattern `(?@p x)`

instead of `?p`

but I am not sure how that would combine with the `context`

pattern...

Oh I did not know about this tactic! Thanks, I will try.

Ah but it's not clear how to use `pattern`

on a subterm…

does `dependent rewrite`

work in your situation?

https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.dependent-rewrite

Or am i misunderstanding what you want to accomplish?

Ah, no, you still would need to formulate `sigT_rewrite`

and rewrite with it, which means you need to give `p`

Yes, that's the problem.

The trick with `set`

seems to be going in the right direction, now I'm trying to match on the body of a local definition, but

```
set (bar := true).
match bar with
| true => idtac
end.
```

fails.

I can do

```
lazymatch goal with
| h := (fun x => @?p x) ?y |- _ => idtac
end.
```

instead.

Théo Winterhalter said:

The trick with

`set`

seems to be going in the right direction, now I'm trying to match on the body of a local definition, but`set (bar := true). match bar with | true => idtac end.`

fails.

you probably need to unfold bar here, no ?

I want to match in the body of a local definition.

But since I know it's the last one, a `lazymatch goal`

works.

yes I mean `let t := eval unfold bar in bar in match t with ...`

Oh.

you want to match the body of bar, not the variable itself

Anyway thanks a lot because it now works:

```
Ltac rewrite_prog e :=
match type of e with
| ?x = _ =>
match goal with
| |- context [ exist ?P ?p ?h ] =>
let foo := fresh "foo" in
set (foo := p) ;
pattern x in foo ;
lazymatch goal with
| h := (fun x => @?p x) ?y |- _ =>
subst foo ;
erewrite (sig_rewrite p _ e)
end
end
end.
```

Ltac... :sweat_smile:

My favourite description of Ltac: Ltac.png

(for those not speaking French: it reads "it is yellow, it is ugly, it doesn't fit to anything, but it saves your life")

it *may* save your life.

Which is even more fitting given that Ltac can also destroy your mental sanity.

I would say two turns are OK with Ltac (before it falls apart) ;-)

@Théo Winterhalter I see you're rewriting inside `exist`

. Can you use proof irrelevance instead?

with sth like `a = b -> exist a h1 = exist b h2`

since `p`

produces a `Prop`

, that's plausible — either by postulating proof irrelevance, or by ensuring it's provable.

There still would be a cast needed, as h is a proof for `x`

, not `y`

.

sorry, I miscounted argument — the proofs are unconstrained

I like to combine the following (from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/proof_irrel.v):

```
Instance eq_pi {A} (x : A) `{∀ z, Decision (x = z)} (y : A) :
ProofIrrel (x = y).
Lemma sig_eq_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
(x y : sig P) : x = y ↔ `x = `y.
```

so as long as your property can be phrased as a decidable equality (say, `compute_property ... = true`

), you're set

what do you mean by 'miscount'?

ah, ok, position offset

hm, confused, not sure I did

I parsed argument as in "semantic evidence"

not as parameter of a function^^

(I always forget whether `exist`

is a type of the constructor for the type)

`exist : sig`

my statements and yours can't match, I have `Arguments exist {_} _ _ _ : assert.`

in scope from stdpp

my context:

```
Print exist.
Inductive sig (A : Type) (P : A → Prop) : Type :=
exist : ∀ x : A, P x → {x : A | P x}
Arguments sig [A]%type_scope _%type_scope
Arguments exist {A}%type_scope _%function_scope
```

moreover, while sth like `a = b -> exist a h1 = exist b h2`

isn't always provable, I'd advice against using sigma types when it isn't.

we talk about ```
Lemma sig_rewrite :
∀ {T A} {P : A → Prop} {x y} (p : T → A) (h : P (p x)) (e : x = y),
exist _ (p x) h = exist _ (p y) (sig_rewrite_aux p h e).
```

, do we?

yes, but we're using different `Arguments`

for `exist`

.

does your `exist a h1 `

have type `sig _ _`

or `_ -> sig _ _`

?

the former — see the `Arguments`

I pasted

in that style, what I'm suggesting becomes:

```
Lemma sig_rewrite :
∀ {T A} {P : A → Prop} {x y} (p : T → A) h1 h2 (e : x = y),
exist _ (p x) h1 = exist _ (p y) h2
```

the point is that `h1`

and `h2`

should be completely unconstrained. Which requires proof irrelevance.

postulated, or proven (see above). Makes sense?

if you don't like stdpp, I'm sure math-comp has the same reasoning principles in their style

I assume proof irrelevance yes. But the fact that the rhs is unconstrained is actually bad for rewriting isn't it? I don't want Coq to ask me to prove the predicate again. That's why I did it the way I did.

Your formulation of sig_rewrite can be used to show that is does not matter which evidence one provides, but I think that is a combination of two reasoning step: One can rewrite in the `h1`

(theos lemma sig_rewrite), and the fact that ```
∀ {A} {P : A → Prop} {z} (h1 h2: P z),
exist _ z h1 = exist _ z h2
```

for proof-irrelevant z.

I don't really see how it helps for rewriting.

paolo's lemma is good when one has two `exist `

tuples for which one wants to establish equality, and theos is good for if one wants to construct a `exist`

tuple for another, equal first component

(Sorry for not writing the 'é')

Ah yes, of course, as a lemma—not for rewriting—the other option is best. And I do have something like this.

Fabian Kunze said:

(Sorry for not writing the 'é')

I don't care. :)

@Théo Winterhalter regarding your `rewrite_prog`

tactic above, you might be interested in the construction `lazymatch (eval pattern x in foo) with ?p ?y => ... end`

(parentheses not necessary)

You might or might not also be interested in the `inversion_sigma`

tactic of the standard library, which knows how to turn an equality `exist P a b = exist P c d`

into two equalities, without using any axioms. (It doesn't go the other way, but there are some lemmas in the standard library which can go in both directions, I believe)

Jason Gross said:

Théo Winterhalter regarding your

`rewrite_prog`

tactic above, you might be interested in the construction`lazymatch (eval pattern x in foo) with ?p ?y => ... end`

(parentheses not necessary)

Oh I wasn't aware of that. That seems much better than posing. Thanks Jason!

Last updated: Oct 05 2023 at 02:01 UTC