Tutorial di Meccanizzazione della Matematicamaggesi/tpcoq/verifica.pdf · 2015. 8. 21. · Tutorial...

Tutorial di Meccanizzazione della Matematica

Marco Maggesi

DiMaI – Dipartimento di Matematica e Informatica“U. Dini”

Agosto 2015

Introduzione a Coq

I Un sistema di dimostrazione interattivo (proof assistant).

I Un linguaggio di programmazione funzionale.

Coq e basato sul Calcolo delle Costruzioni Induttive (CIC).

Alcune notazioni

1. f x ≡ f (x)

2. f x y ≡ f (x , y)

3. f (g t) t ≡ f (g(t), t)

4. f : nat -> nat ≡ f : N −→ N

5. ~A ≡ ¬A6. A -> B ≡ A =⇒ B

7. A <-> B ≡ A ⇐⇒ B

8. A /\ B ≡ A ∧ B

9. A \/ B ≡ A ∨ B

10. forall x : A. P x ≡ ∀x ∈ A.P(x)

11. exists x : A. P x ≡ ∃x ∈ A.P(x)

Alcune notazioni

1. f x ≡ f (x)

2. f x y ≡ f (x , y)

3. f (g t) t ≡ f (g(t), t)

4. f : nat -> nat ≡ f : N −→ N5. ~A ≡ ¬A6. A -> B ≡ A =⇒ B

7. A <-> B ≡ A ⇐⇒ B

8. A /\ B ≡ A ∧ B

9. A \/ B ≡ A ∨ B

Alcune notazioni

1. f x ≡ f (x)

2. f x y ≡ f (x , y)

3. f (g t) t ≡ f (g(t), t)

4. f : nat -> nat ≡ f : N −→ N5. ~A ≡ ¬A6. A -> B ≡ A =⇒ B

7. A <-> B ≡ A ⇐⇒ B

8. A /\ B ≡ A ∧ B

9. A \/ B ≡ A ∨ B

I tipi di Coq

In Coq ogni termine ha un tipo univocamente individuato.

Check 0.

0 : nat

Check nat.

nat : Set

Check 2+2=4.

2 + 2 = 4 : Prop

Check True.

True : Prop

Check Prop.

Prop : Type

I tipi di Coq

Check 0.

0 : nat

Check nat.

nat : Set

Check 2+2=4.

2 + 2 = 4 : Prop

Check True.

True : Prop

Check Prop.

Prop : Type

I tipi di Coq

Check 0.

0 : nat

Check nat.

nat : Set

Check 2+2=4.

2 + 2 = 4 : Prop

Check True.

True : Prop

Check Prop.

Prop : Type

I tipi di Coq

Check 0.

0 : nat

Check nat.

nat : Set

Check 2+2=4.

2 + 2 = 4 : Prop

Check True.

True : Prop

Check Prop.

Prop : Type

Dichiarazioni

Section Dichiarazioni.

Variable n : nat.

n is assumed

Hypothesis Pos_n : (gt n 0).

Pos_n is assumed

Check gt.

gt : nat -> nat -> Prop

Check (gt n 0).

n > 0 : Prop

Dichiarazioni

Variable n : nat.

n is assumed

Pos_n is assumed

Check gt.

Check (gt n 0).

n > 0 : Prop

Dichiarazioni

Variable n : nat.

n is assumed

Pos_n is assumed

Check gt.

Check (gt n 0).

n > 0 : Prop

Defininizioni

Definition one : nat := S 0.

one is defined

Definition two : nat := S one.

two is defined

Print one.

one = 1 : nat

Definition double (m : nat) := plus m m.

double is defined

Print double.

double = fun m : nat => m + m : nat -> nat

Defininizioni

one is defined

two is defined

Print one.

one = 1 : nat

double is defined

Print double.

Defininizioni

one is defined

two is defined

Print one.

one = 1 : nat

double is defined

Print double.

Defininizioni

one is defined

two is defined

Print one.

one = 1 : nat

double is defined

Print double.

Logica proposizionale

Section Esempi_logica.

Variable A B C : Prop.

A is assumed.

B is assumed.

C is assumed.

Check (A -> B)

A -> B : Prop

Lemma es1: (A -> B -> C) -> (A -> B) -> (A -> C).

1 subgoal

A : Prop

B : Prop

C : Prop

============================

(A -> B -> C) -> (A -> B) -> A -> C

A is assumed.

B is assumed.

C is assumed.

Check (A -> B)

A -> B : Prop

Lemma es1: (A -> B -> C) -> (A -> B) -> (A -> C).

1 subgoal

A : Prop

B : Prop

C : Prop

============================

(A -> B -> C) -> (A -> B) -> A -> C

A is assumed.

B is assumed.

C is assumed.

Check (A -> B)

A -> B : Prop

Lemma es1: (A -> B -> C) -> (A -> B) -> (A -> C).

1 subgoal

A : Prop

B : Prop

C : Prop

============================

(A -> B -> C) -> (A -> B) -> A -> C

Logica proposizionale (continua)

intros H H’ HA.

1 subgoal

A : Prop

B : Prop

C : Prop

H : A -> B -> C

H’ : A -> B

HA : A

============================

apply H.

2 subgoals

A : Prop

B : Prop

C : Prop

H : A -> B -> C

H’ : A -> B

HA : A

============================

subgoal 2 is:

apply HA.

1 subgoal

A : Prop

B : Prop

C : Prop

H : A -> B -> C

H’ : A -> B

HA : A

============================

apply H’.

1 subgoal

A : Prop

B : Prop

C : Prop

H : A -> B -> C

H’ : A -> B

HA : A

============================

apply HA.

Proof completed.

es1 is defined

Check es1.

: (A -> B -> C) -> (A -> B) -> A -> C

apply HA.

Proof completed.

es1 is defined

Check es1.

: (A -> B -> C) -> (A -> B) -> A -> C

apply HA.

Proof completed.

es1 is defined

Check es1.

: (A -> B -> C) -> (A -> B) -> A -> C

1 subgoal

A : Prop

B : Prop

C : Prop

============================

(A -> B -> C) -> (A -> B) -> A -> C

Proof completed.

es1_bis is defined

1 subgoal

A : Prop

B : Prop

C : Prop

============================

(A -> B -> C) -> (A -> B) -> A -> C

Proof completed.

es1_bis is defined

1 subgoal

A : Prop

B : Prop

C : Prop

============================

(A -> B -> C) -> (A -> B) -> A -> C

Proof completed.

es1_bis is defined

Alcune tattiche di Coq (calcolo proposizionale)

1. apply thm: applica thm.

2. intro H: introduce una ipotesi chiamandola H.

3. intros: introduce tutte le ipotesi.

4. unfold nome: sostituisce la costante nome con la suadefinizione.

5. left / right: distrugge la tesi della forma A ∨ B.

6. split: distrugge la tesi della forma A ∧ B, A ⇐⇒ B.

Alcune tattiche di Coq (uguaglianza)

1. reflexivity: dimostra x = x .

2. symmetry: riduce x = y a y = x .

3. transitivity x : riduce a = b a a = x e x = b.

4. rewrite thm: riscrive l’equazione thm.

Alcune tattiche di Coq (dimostrazione automatica)

1. auto: usa fatti gia noti.

2. tauto: dimostra una tautologia.

3. intuition: auto + tauto.

4. firstorder: dimostra una semplice proposizione del primoordine.

Per iniziare

Collegatevi alla pagina

http://www.math.unifi.it/users/maggesi/tpcoq2015/

I file di lavoro sono quelli con estensione .v .Scaricateli sul vostro computer ed aprirteli con Coq.

Tutorial di Meccanizzazione della Matematicamaggesi/tpcoq/verifica.pdf · 2015. 8. 21. · Tutorial...

Documents

Transcript of Tutorial di Meccanizzazione della Matematicamaggesi/tpcoq/verifica.pdf · 2015. 8. 21. · Tutorial...