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

apartes

 
m1ilc/preuves_egalite.txt · Dernière modification: 2010/05/19 09:59 par suitable
 
Sauf mention contraire, le contenu de ce wiki est placé sous la licence suivante :CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki