come nominare l'assunto quando si ricorda un'espressione?

Question

La documentazione per Coq reca l'ammonizione generale non per fare affidamento sul meccanismo di denominazione incorporato, ma selezionare i propri nomi, per evitare che le modifiche nel meccanismo di denominazione rendano invalide le prove passate.

Quando si considerano le espressioni del modulo remember Expr as v, impostiamo la variabile v nell'espressione Expr. Ma il nome del presupposto viene selezionato automaticamente, ed è qualcosa di simile a Heqv, quindi abbiamo:

Heqv: v = Expr

Come posso scegliere il mio nome al posto di Heqv? Posso sempre rinominarlo con qualsiasi cosa mi piaccia usando il comando rename, ma questo non mantiene le mie dimostrazioni indipendenti dalle ipotetiche modifiche future nel meccanismo di denominazione incorporato in Coq.

Answer 1

Se è possibile eliminare l'uguaglianza separata, provare set (name := val). Utilizzare unfold anziché rewrite per ripristinare il valore.

Se è necessaria l'uguaglianza per oltre lo rewrite <-, non conosco alcuna tattica incorporata che faccia questo. Puoi farlo manualmente, però, o costruire una tattica/notazione. L'ho appena buttato insieme. (Nota: io non sono un esperto, questo potrebbe essere fatto più facilmente.)

Tactic Notation "remember_as_eq" constr(expr) ident(vname) ident(eqname) := 
    let v  := fresh in 
    let HHelp := fresh in 
    set (v := expr); 
    (assert (HHelp : sigT (fun x => x = v)) by (apply (existT _ v); reflexivity)); 
    inversion HHelp as [vname eqname]; 
    unfold v in *; clear v HHelp; 
    rewrite <- eqname in *. 

Usa come remember_as_eq (2+2) four Heqfour per ottenere lo stesso risultato con remember (2+2) as four.

---

Nota: aggiornato per gestire più casi, la vecchia versione fallito su alcune combinazioni di valore e il tipo di obiettivo. Lascia un commento se trovi un altro caso che funziona con rewrite ma non questo.