6
In coq, è in qualche modo possibile applicare un lemma o un'ipotesi a una sottoespressione dell'obiettivo corrente? Per esempio vorrei applicare il fatto che plus è commutativo per scambiare 3 e 4 in questo esempio.Come utilizzare la riscrittura su una sottoespressione dell'obiettivo corrente
Require Import Coq.Arith.Plus.
Inductive foobar : nat -> Prop :=
| foob : forall n:nat, foobar n.
Goal foob (3 + 4) = foob (4 + 3).
Proof.
apply plus_comm. (* or maybe rewrite plus_comm *)
dà:
Error: Impossible to unify "?199 + ?200 = ?200 + ?199" with
"foob (3 + 4) = foob (4 + 3)".
Come posso dire a coq dove proprio in questo obiettivo di applicare plus_comm?
Funziona quando faccio quanto segue, che è quello che volevo provare in primo luogo. Goal foobar (3 + 4) = foobar (4 + 3). Prova. riscrivi plus_comm. riflessività. Qed. Immagino che la riscrittura non funzioni sui valori, solo sui tipi. –
'rewrite' funziona su entrambi (in realtà i tipi sono termini in Coq ;-). Il problema principale qui è che 'foob (3 + 4)' ha tipo 'foobar (3 + 4)' e 'foob (4 + 3)' ha tipo 'foobar (4 + 3)'. Coq può controllare che entrambi siano uguali (quindi l'uguaglianza è ben tipizzata), ma 'rewrite' usa una forma intermedia in cui non è il caso, da qui il messaggio di errore criptico che si ottiene con' rewrite (plus_comm 3 4) '. – Virgile
Normalmente, dovresti essere in grado di usare 'pattern' (http://coq.inria.fr/refman/Reference-Manual011.html#pattern) per azioni locali da qualche parte all'interno del termine. Tuttavia, ciò non riesce per la stessa ragione menzionata da @Virgile. Se ciò è possibile, puoi anche passare temporaneamente ad un tipo di uguaglianza "più completo" (ad es. 'JMeq'), fare cose lì e poi tornare indietro. (Mi piace considerarlo come il "numero complesso" - analogo dell'uguaglianza). – nobody