===== L'égalité en Coq =====

  Check eq.
  eq : forall A : Type, A -> A -> Prop
  Check refl_equal.
  refl_equal : forall (A : Type) (x : A), x = x

C'est un type polymorphe (A:Type). Cela signifie que l'on a une relation d'égalité générique dont le premier argument est le type des éléments à comparer.

L'égalité est une relation réflexive, symétrique et transitive. Ces propriétés sont utilisables grâce aux tactiques reflexivity, symmetry et transitivity t.

==== Égalité de Leibniz ====

  Check eq_ind.
  eq_ind : forall (A : Type) (x : A) (P : A -> Prop),
  P x -> forall y : A, x = y -> P y

Si x = y, tous ce qui est vrai pour x est vrai pour y, si j'ai compris.

==== Les tactiques pour l'égalité ====

  rewrite
  rewrite in
  replace with
  replace with in
  subst

|  H: a = 2b+1  \\ ------  \\ a + 2 = 3x ^ rewrite H | H: a = 2b+1  \\ ------ \\ 2b+1 + 2 = 3x  |
^  -:-  ^^^
|  H : 2x+1 = b \\ H2: x=z ^ rewrite H2 in H  | H : 2z+1=b \\ x=z  |
^  -:-  ^^^
| H:  a=2*b \\ H2: a=5 \\ ------ \\ a=2*x+1 ^ replace (2*b) with 5  | H: a=2*b  \\ H2: a=5 \\ ------ (1/2) \\ a=5+1 \\   \\ H: a=2*b  \\ H2: a=5 \\ ------(2/2) \\ 2*b=5 |
| H: a=2*b  \\ H2: a=5 \\ ------(2/2) \\ 2*b=5 ^ rewrite H2 in H | H: 5=2*b  \\ H2: a=5 \\ ------(2/2) \\ 2*b=5 |
|  ^ rewrite H  |  H: 2*b=5  \\ H2: a=5 \\ ------ \\ 2*b=2*b  |
|  ^ rewrite <- H | 5=5  |
|  ^ reflexivity  |  |
| H: a=2*b  \\ H2: a=5 \\ ------ \\ 5=2*b ^ symmetry.\\ assumption. |  |
^  -:-  ^^^
| H: x = a+b \\ H2: 2*x+3=5 \\ H3: 2*x+7=z \\ ------ \\ z + 2*x = 0 ^  subst x  | 2*(a+b)+3=5 \\ 2*(a+b)+7=z \\ ------ \\ z+2*(a+b) = 0 |


   

[[preuves_4#apartes|]]