UP | HOME

Übersicht: Coq für Aussagen– und Prädikatenlogik Erster Ordnung

Diese Tabelle versucht systematisch verschiedene Coq Strategien (bzw. Operationen) darzustellen. Hierbei wird gezeigt, wie diese einem Helfen können Folgerungen zu schließen, um mittels Aussagen im Kontext zu einem gewünschtem (Zwischen-)Ziel zu kommen.

Basierend auf Übungsaufzeichnungen aus GLoIn, 2018/19.

Operation Ziel Kontext Fitch-Analogie
apply H. Φ ⇒ ■ H: Φ ⊥I
Φ ⇒ Ψ H: Φ ⇒ Ψ
Φ ⇒ Ψ H: ∀x. (Ψ(x) ⇒ Φ(x))
apply NNPP. q ⇒ ¬ ¬ q N/A ¬E
exact H.1
assumption. 		Φ ⇒ ■ H: Φ N/A
intro A. Φ → Ψ ⇒ Ψ ⇒ A: Φ ¬I
∀x. Φ ⇒ Φ ⇒ x2
assert (Φ). Ψ ⇒ subgoal
⇒ Φ 		N/A N/A
split. Φ ∧ Ψ ⇒3 Φ N/A ∧I
contradiction. Φ ⇒ ■ H1: Φ
H2: ¬ Φ 		⊥E
left. Φ ∨ Ψ ⇒ Ψ N/A ∨I1
right. Φ ∨ Ψ ⇒ Φ N/A ∨I2
destruct. N/A H: Φ ∧ Ψ ⇒ H1: Φ
H2: Ψ 		N/A4
H: ∃ x. Φ(x) ⇒ x0: …
H: Φ(x0)
exists x0. ∃ x. Φ(x) ⇒ Φ(x0) N/A N/A

Weiteres Material

1: Analog zum erstem apply H. Fall.

2: Sei x beliebig.

3: Ψ wird zum subgoal.

4: destruct kann auch mit dem as-Schlüsselwort erweitert werden, indem nach as ein Muster für Konjunktionen und Disjunktionen beschrieben wird, die jeweils mit Leerzeichen und einem senkrechtem Strich.

Bspw. x0 ∧ x1 ∧ x2 ∨ y0 ∨ z0 ∧ z1 kann mit [X0 X1 X2 | Y0 | Z0 Z1] aufgespalten werden (wo dann x0 für X0 steht, usw.).

Wird dieses gemacht, bewirkt man eine Und oder Oder Elimination (∧E, ∨E).

Siehe auch: Coq Reference Manaual, zu Case analysis and induction.