Vergleich von Coq mit Lean

Inhaltsverzeichnis

  1. Allgemeines
    1. Konstanten
    2. Funktionen
    3. Rekursiv definierte Funktionen
  2. Aussagenlogik
    1. Subjunktionen
    2. Negationen
    3. Konjunktionen
    4. Disjunktionen
    5. Bijunktionen
  3. Prädikatenlogik
    1. Allquantifizierungen

Allgemeines

Konstanten

Coq Lean 
Definition zero: nat := 0.
Check zero.
Compute zero + 1.

def zero: Nat := 0
#check zero
#eval zero + 1

Funktionen

Coq Lean 
Definition f: ∀T: Type, T → T :=
  fun T (x: T) => x.

def f: ∀T: Type, T → T :=
  fun T (x: T) => x

Definition f (T: Type) (x: T): T := x.

def f (T: Type) (x: T): T := x

Rekursiv definierte Funktionen

Coq Lean 
Fixpoint f (n: nat): nat :=
  match n with
  | 0 => 1
  | S n => (S n)*(f n)
  end.

Compute f 4.

def f (n: Nat): Nat :=
  match n with
  | 0 => 1
  | Nat.succ n => (Nat.succ n)*(f n)

#eval f 4

Aussagenlogik

Subjunktionen

Beweisterme für Subjunktionen

Coq Lean 
Theorem subj_id (A B: Prop): A -> A.
Proof fun h => h.

theorem subj_id (A B: Prop): A → A :=
  fun h => h

Theorem subj_elim (A B: Prop):
  A -> (A -> B) -> B.
Proof
  fun hA => fun hAB => hAB hA.

theorem subj_elim (A B: Prop):
  A → (A → B) → B
:=
  fun hA => fun hAB => hAB hA

Taktiken für Subjunktionen

Coq Lean 
Theorem subj_id (A: Prop):
  A -> A.
Proof.
  intro h.
  exact h.
Qed.

theorem subj_id (A: Prop):
  A → A
:= by
  intro h
  exact h

Theorem subj_id (A: Prop): A -> A.
Proof.
  intro h. exact h.
Qed.

theorem subj_id (A: Prop): A → A := by
  intro h; exact h

Theorem subj_elim (A B: Prop):
  A -> (A -> B) -> B.
Proof.
  intros hA hAB. apply hAB.
  exact hA.
Qed.

theorem subj_elim (A B: Prop):
  A → (A → B) → B
:= by
  intro hA hAB; apply hAB
  exact hA

Negationen

Beweisterme für Negationen

Coq Lean 
Theorem neg_intro (A: Prop):
  (A -> False) -> ~A.
Proof
  fun h => fun hA => h hA.

theorem neg_intro (A: Prop):
  (A → False) → ¬A
:=
  fun h => fun hA => h hA

Theorem neg_elim (A: Prop):
  A -> ~A -> False.
Proof
  fun hA => fun hnA => hnA hA.

theorem neg_elim (A: Prop):
  A → ¬A → False
:=
  fun hA => fun hnA => hnA hA

Taktiken für Negationen

Coq Lean 
Theorem neg_intro (A: Prop):
  (A -> False) -> ~A.
Proof.
  intro h. intro hA.
  apply h. exact hA.
Qed.

theorem neg_intro (A: Prop):
  (A → False) → ¬A
:= by
  intro h; intro hA
  apply h; exact hA

Theorem neg_elim (A: Prop):
  A -> ~A -> False.
Proof.
  intros hA hnA. apply hnA. exact hA.
Qed.

theorem neg_elim (A: Prop):
  A → ¬A → False
:= by
  intro hA hnA; apply hnA; exact hA

Konjunktionen

Beweisterme für Konjunktionen

Coq Lean
conj: ∀{A B: Prop}, A → B → A ∧ B And.intro {a b: Prop} (left: a) (right: b): a ∧ b
proj1: ∀{A B: Prop}, A ∧ B → A And.left {a b: Prop} (self: a ∧ b): a
proj2: ∀{A B: Prop}, A ∧ B → B And.right {a b: Prop} (self: a ∧ b): b

Taktiken für Konjunktionen

Coq Lean 
Theorem conj_intro (A B: Prop):
  A -> B -> A /\ B.
Proof.
  intros hA hB.
  split.
  * exact hA.
  * exact hB.
Qed.

theorem conj_intro (A B: Prop):
  A → B → A ∧ B
:= by
  intro hA hB
  apply And.intro
  . exact hA
  . exact hB

Theorem conj_eliml (A B: Prop):
  A /\ B -> A.
Proof.
  intro h.
  destruct h as (hA, _). exact hA.
Qed.

theorem conj_eliml (A B: Prop):
  A ∧ B → A
:= by
  intro h
  cases h with
  | intro hA _ => exact hA

Theorem conj_eliml (A B: Prop):
  A /\ B -> A.
Proof.
  intro h.
  assert (hA := proj1 h).
  exact hA.
Qed.

theorem conj_eliml (A B: Prop):
  A ∧ B → A
:= by
  intro h
  have hA := h.left
  exact hA

Disjunktionen

Taktiken für Disjunktionen

Coq Lean 
Theorem disj_introl (A B: Prop):
  A -> A \/ B.
Proof.
  intro h. left. exact h.
Qed.

theorem disj_introl (A B: Prop):
  A → A ∨ B
:= by
  intro h; left; exact h

Theorem disj_elim (A B C: Prop):
  A \/ B -> (A -> C) -> (B -> C) -> C.
Proof.
  intros h hAC hBC.
  destruct h as [hl | hr].
  * apply hAC. exact hl.
  * apply hBC. exact hr.
Qed.

theorem disj_elim (A B C: Prop):
  A ∨ B → (A → C) →  (B → C) → C
:= by
  intro h hAC hBC
  cases h
  case inl hl =>
    apply hAC; exact hl
  case inr hr =>
    apply hBC; exact hr

Bijunktionen

Beweisterme für Bijunktionen

Coq Lean 
Theorem bij_intro (A B: Prop):
  (A -> B) -> (B -> A) -> (A <-> B).
Proof
  fun hAB => fun hBA => conj hAB hBA.

theorem bij_intro (A B: Prop):
  (A → B) → (B → A) → (A ↔ B)
:=
  fun hAB ↦ fun hBA ↦ Iff.intro hAB hBA

Theorem bij_eliml (A B: Prop):
  (A <-> B) -> (A -> B).
Proof
  fun h => proj1 h.

theorem bij_eliml (A B: Prop):
  (A ↔ B) → (A → B)
:=
  fun h ↦ h.1

Taktiken für Bijunktionen

Coq Lean 
Theorem bij_intro (A B: Prop):
  (A -> B) -> (B -> A) -> (A <-> B).
Proof.
  intros hAB hBA.
  split.
  * exact hAB.
  * exact hBA.
Qed.

theorem bij_intro (A B: Prop):
  (A → B) → (B → A) → (A ↔ B)
:= by
  intro hAB hBA
  apply Iff.intro
  . exact hAB
  . exact hBA

Theorem bij_eliml (A B: Prop):
  (A <-> B) -> (A -> B).
Proof.
  intro h.
  assert (hAB := proj1 h).
  exact hAB.
Qed.

theorem bij_eliml (A B: Prop):
  (A ↔ B) → (A → B)
:= by
  intro h
  have hAB := h.1
  exact hAB

Prädikatenlogik

Allquantifizierungen

Beweisterme für Allquantifizierungen

Coq Lean 
Theorem uq_id (X: Type) (P: X -> Prop):
  forall x: X, P x -> P x.
Proof
  fun x => fun hx => hx.

theorem uq_id (X: Type) (P: X → Prop):
  ∀x: X, P x → P x
:=
  fun _x => fun hx => hx

Theorem uq_mp (X: Type) (P Q: X -> Prop):
  (forall x: X, P x -> Q x) ->
  (forall x: X, P x) ->
  (forall x: X, Q x).
Proof
  fun hPQ hP x => (hPQ x) (hP x).

theorem uq_mp (X: Type) (P Q: X → Prop):
  (∀x: X, P x → Q x) →
  (∀x: X, P x) →
  (∀x: X, Q x)
:=
  fun hPQ hP x => (hPQ x) (hP x)

Taktiken für Allquantifizierungen

Coq Lean 
Theorem uq_id (X: Type) (P: X -> Prop):
  forall x: X, P x -> P x.
Proof.
  intros x hx. exact hx.
Qed.

theorem uq_id (X: Type) (P: X → Prop):
  ∀x: X, P x → P x
:= by
  intro x hx; exact hx

Theorem uq_mp (X: Type) (P Q: X -> Prop):
  (forall x: X, P x -> Q x) ->
  (forall x: X, P x) ->
  (forall x: X, Q x).
Proof.
  intros hPQ hP. intro x.
  apply (hPQ x). exact (hP x).
Qed.

theorem uq_mp (X: Type) (P Q: X → Prop):
  (∀x: X, P x → Q x) →
  (∀x: X, P x) →
  (∀x: X, Q x)
:= by
  intro hPQ hP; intro x
  apply hPQ x; exact hP x