Rewriting in Σ-types · Coq users

Stream: Coq users

Topic: Rewriting in Σ-types

Théo Winterhalter (Dec 16 2020 at 18:57):

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.

Kenji Maillard (Dec 16 2020 at 19:06):

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

Théo Winterhalter (Dec 16 2020 at 19:28):

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

Théo Winterhalter (Dec 16 2020 at 19:31):

Ah but it's not clear how to use pattern on a subterm…

Fabian Kunze (Dec 16 2020 at 20:24):

does dependent rewrite work in your situation?
https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.dependent-rewrite

Fabian Kunze (Dec 16 2020 at 20:25):

Or am i misunderstanding what you want to accomplish?

Fabian Kunze (Dec 16 2020 at 20:27):

Ah, no, you still would need to formulate sigT_rewrite and rewrite with it, which means you need to give p

Théo Winterhalter (Dec 16 2020 at 21:21):

Yes, that's the problem.

Théo Winterhalter (Dec 16 2020 at 21:29):

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.

Théo Winterhalter (Dec 16 2020 at 21:31):

I can do

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

instead.

Kenji Maillard (Dec 16 2020 at 21:34):

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 ?

Théo Winterhalter (Dec 16 2020 at 21:34):

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

Théo Winterhalter (Dec 16 2020 at 21:35):

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

Kenji Maillard (Dec 16 2020 at 21:35):

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

Théo Winterhalter (Dec 16 2020 at 21:35):

Oh.

Kenji Maillard (Dec 16 2020 at 21:36):

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

Théo Winterhalter (Dec 16 2020 at 21:36):

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.

Kenji Maillard (Dec 16 2020 at 21:36):

Ltac... :sweat_smile:

Michael Soegtrop (Dec 17 2020 at 11:38):

My favourite description of Ltac: Ltac.png

Michael Soegtrop (Dec 17 2020 at 11:41):

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

Pierre-Marie Pédrot (Dec 17 2020 at 11:46):

it may save your life.

Pierre-Marie Pédrot (Dec 17 2020 at 11:47):

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

Emilio Jesús Gallego Arias (Dec 17 2020 at 13:59):

ltac.gif

Michael Soegtrop (Dec 17 2020 at 14:27):

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

Paolo Giarrusso (Dec 18 2020 at 18:30):

@Théo Winterhalter I see you're rewriting inside exist. Can you use proof irrelevance instead?

Paolo Giarrusso (Dec 18 2020 at 18:31):

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

Paolo Giarrusso (Dec 18 2020 at 18:32):

since p produces a Prop, that's plausible — either by postulating proof irrelevance, or by ensuring it's provable.

Fabian Kunze (Dec 18 2020 at 18:34):

There still would be a cast needed, as h is a proof for x, not y.

Paolo Giarrusso (Dec 18 2020 at 18:35):

sorry, I miscounted argument — the proofs are unconstrained

Paolo Giarrusso (Dec 18 2020 at 18:36):

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

Fabian Kunze (Dec 18 2020 at 18:37):

what do you mean by 'miscount'?

Fabian Kunze (Dec 18 2020 at 18:37):

ah, ok, position offset

Paolo Giarrusso (Dec 18 2020 at 18:37):

hm, confused, not sure I did

Fabian Kunze (Dec 18 2020 at 18:37):

I parsed argument as in "semantic evidence"

Fabian Kunze (Dec 18 2020 at 18:38):

not as parameter of a function^^

Fabian Kunze (Dec 18 2020 at 18:38):

(I always forget whether exist is a type of the constructor for the type)

Paolo Giarrusso (Dec 18 2020 at 18:39):

exist : sig

Paolo Giarrusso (Dec 18 2020 at 18:39):

my statements and yours can't match, I have Arguments exist {_} _ _ _ : assert. in scope from stdpp

Paolo Giarrusso (Dec 18 2020 at 18:39):

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

Paolo Giarrusso (Dec 18 2020 at 18:40):

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.

Fabian Kunze (Dec 18 2020 at 18:40):

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?

Paolo Giarrusso (Dec 18 2020 at 18:40):

yes, but we're using different Arguments for exist.

Fabian Kunze (Dec 18 2020 at 18:41):

does your exist a h1 have type sig _ _ or _ -> sig _ _?

Paolo Giarrusso (Dec 18 2020 at 18:42):

the former — see the Arguments I pasted

Paolo Giarrusso (Dec 18 2020 at 18:42):

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

Paolo Giarrusso (Dec 18 2020 at 18:42):

the point is that h1 and h2 should be completely unconstrained. Which requires proof irrelevance.

Paolo Giarrusso (Dec 18 2020 at 18:43):

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

Paolo Giarrusso (Dec 18 2020 at 18:44):

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

Théo Winterhalter (Dec 18 2020 at 18:51):

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.

Fabian Kunze (Dec 18 2020 at 18:51):

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.

Théo Winterhalter (Dec 18 2020 at 18:52):

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

Fabian Kunze (Dec 18 2020 at 18:52):

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

Fabian Kunze (Dec 18 2020 at 18:53):

(Sorry for not writing the 'é')

Théo Winterhalter (Dec 18 2020 at 18:53):

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

Théo Winterhalter (Dec 18 2020 at 18:53):

Fabian Kunze said:

(Sorry for not writing the 'é')

I don't care. :)

Jason Gross (Jan 01 2021 at 13:25):

@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)

Jason Gross (Jan 01 2021 at 13:26):

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)

Théo Winterhalter (Jan 01 2021 at 15:22):

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