Coq comment bien imprimer un terme construit en utilisant des tactiques?

Question

Je suis nouveau à Coq et je fais quelques exercices pour me familiariser avec ça. Ma compréhension est que prouver une proposition dans Coq "vraiment" est écrire un type dans Gallina et montrer ensuite qu'il est habité en utilisant des tactiques pour combiner des termes de manière déterministe.

Je me demande s'il existe un moyen d'obtenir une représentation assez bien imprimée du terme réel, avec toutes les tactiques supprimées.

Dans l'exemple ci-dessous, un terme anonyme de type plus_comm (x y : N) : plus x y = plus y x est finalement produit ... Je pense. Que dois-je faire si je veux le regarder? Dans un certain sens, je suis curieux de savoir à quoi la tactique "désole".

Voici le code en question, extrait littéralement d'un tutoriel sur YouTube https://www.youtube.com/watch?v=OaIn7g8BAIc.

Inductive N : Type := 
| O : N 
| S : N -> N 
. 

Fixpoint plus (x y : N) : N := 
match x with 
| O => y 
| S x' => S (plus x' y) 
end. 

Lemma plus_0 (x : N) : plus x O = x. 

Proof. 
    induction x. 
    - simpl. reflexivity. 
    - simpl. rewrite IHx. reflexivity. 
Qed. 

Lemma plus_S (x y : N) : plus x (S y) = S(plus x y). 

Proof. 
    induction x. 
    - simpl. reflexivity. 
    - simpl. rewrite IHx. reflexivity. 
Qed. 


Lemma plus_comm (x y : N) : plus x y = plus y x. 

Proof. 
    induction x. 
    - simpl. rewrite plus_0. reflexivity. 
    - simpl. rewrite IHx. rewrite plus_S. reflexivity. 
Qed. 

Answer 1

Tout d'abord, plus_comm est pas une partie du type. Vous obtenez un terme nomméplus_comm de type forall x y : N, plus x y = plus y x. Vous pouvez vérifier à l'aide de la commande suivante

Check plus_comm. 

Ainsi, une autre façon de définir le lemme plus_comm est

Lemma plus_comm : forall x y : N, plus x y = plus y x. 

Comme une note de côté: en Dans ce cas, vous devrez ajouter intros x y. (ou simplement intros.) après la partie Proof.. Les tactiques (et les moyens de les coller ensemble) sont un métalangage appelé Ltac, car elles sont utilisées pour produire des termes d'un autre langage, appelé Gallina, qui est le langage de spécification de Coq.

Par exemple, forall x y : N, plus x y = plus y x est une instance de la phrase Gallina ainsi que le corps de la fonction plus. Pour obtenir le terme attaché à plus_comm utiliser la commande Print:

Print plus_comm. 

plus_comm = 
fun x y : N => 
N_ind (fun x0 : N => plus x0 y = plus y x0) 
    (eq_ind_r (fun n : N => y = n) eq_refl (plus_0 y)) 
    (fun (x0 : N) (IHx : plus x0 y = plus y x0) => 
    eq_ind_r (fun n : N => S n = plus y (S x0)) 
    (eq_ind_r (fun n : N => S (plus y x0) = n) eq_refl (plus_S y x0)) 
    IHx) x 
    : forall x y : N, plus x y = plus y x 

Il n'est pas une lecture facile, mais avec une certaine expérience, vous serez en mesure de le comprendre.

Soit dit en passant, voici comment nous avons pu prouver le lemme de ne pas utiliser la tactique:

Definition plus_comm : forall x y : N, plus x y = plus y x := 
    fix IH (x y : N) := 
    match x return plus x y = plus y x with 
    | O => eq_sym (plus_0 y) 
    | S x => eq_ind _ (fun p => S p = plus y (S x)) (eq_sym (plus_S y x)) _ (eq_sym (IH x y)) 
    end. 

Pour expliquer quelques petites choses: fix est le moyen de définir les fonctions récursives, eq_sym est utilisé pour changer x = y en y = x, et eq_ind correspond à la tactique rewrite.