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