Library hydras.MoreAck.FolExamples

Use of FOL notations (Experimental)

From Coq Require Import Arith Lists.List.

From hydras.Ackermann
Require Import fol folProp folProof Languages folLogic
folLogic2 folLogic3 subAll Deduction primRec.
Import ListNotations.
Import FolNotations.

Preliminary lemmas

#[local] Arguments Ensembles.In {_} .
#[local] Arguments Ensembles.Add {_} .
#[local] Arguments atomic _ _ _ : clear implicits.
#[local] Arguments apply _ _ _ : clear implicits.

About Term_Terms_rec_full.
About Formula_rect.

About Formula_depth_rec.

depth-order vs structural order

Section depth_rec_demo.
Variable L: Language.
Variable P: fol.Formula L → Prop.
Variable a: fol.Formula L.
Goal P a.
Goal P a.

End depth_rec_demo.
Import Ensembles.

Lemma In_add1 {T:Type}(a:T)(S: Ensemble T):
In (Add S a) a.

Lemma In_add2 {T:Type}(a b:T)(S : Ensemble T):
In S a → In (Add S b) a.

#[local] Hint Unfold mem: core.
#[local] Hint Resolve In_add1 In_add2 AXM: core.

fol_scope allows us to read and write FOL terms and formulas in a syntax close to Coq's

Remark R1 L (t: Term L): (equal t t ) = (t = t)%fol.

A small variation on MP (without appending contexts)

Lemma MPSys L (G: System L) (A B: Formula L) :
SysPrf L G (A → B)%fol → SysPrf L G A → SysPrf L G B.

A small language

Module Toy.
  Inductive Rel: Set := A_ | B_ | C_ | P_ | Q_ | R_.
  Inductive Fun : Set := a_ | b_ | f_ | g_ | h_.

  Definition arityR (x : Rel): nat :=
    match x with
       P_ | Q_ ⇒ 1 | R_ ⇒ 2 | _ ⇒ 0
    end.

Definition arityF (x : Fun): nat :=
    match x with f_ | g_ ⇒ 1 | h_ ⇒ 2 | _ ⇒ 0 end.

Definition L := language Rel Fun arityR arityF.

Notation a := (apply L a_ Tnil).
Notation b := (apply L b_ Tnil).
Notation f t := (apply L f_ (Tcons t Tnil)).
Notation g t := (apply L g_ (Tcons t Tnil)).
Notation h t1 t2 := (apply L h_ (Tcons t1 (Tcons t2 Tnil))).

Example t0 : Term L := a.

Example t1 : Term L := f t0.

Example t2 : Term L := h t1 t0.

Example t3 : Term L := h (f (var 0)) (g (var 1)).

Goal t0 = a.
Goal t1 = f a.
Goal t2 = h (f a ) a.

Abreviations for the toy language L

  Notation A := (atomic L A_ Tnil).
  Notation B := (atomic L B_ Tnil).
  Notation C := (atomic L C_ Tnil).
  Notation P t := (atomic L P_ (Tcons t Tnil)).
  Notation Q t := (atomic L Q_ (Tcons t Tnil)).
  Notation R t1 t2 := (@atomic L R_ (Tcons t1 (Tcons t2 Tnil))).

Example F1 : Formula L := R a b.

Example F2 : Formula L :=
  forallH 0 (forallH 1
               (impH (R (var 0) (var 1)) (R (var 1) (var 0)))).

Example F3 : Formula L :=
  forallH 0 (orH (equal (var 0) a)
               (existH 1 (equal (var 0) (f (var 1))))).

Example F4: Formula L :=
  orH (forallH 1 (equal (var 0) (var 1)))
    (existH 0 (existH 1 (notH (equal (var 0) (var 1))))).

Example F5: Formula L := (v #0 = a ∨ v #0 = f v #1)%fol.

Example F6: Formula L:= (allH 0, exH 1, v #0 = f v #1 ∧ v #0 ≠ v #1)%fol.

Print F1.

Print F2.

Print F3.

The following computation expands some derived connectives and quantifiers. Within fol_scope, we print them with a similar syntax (with primed symbols)

Section PrimedSymbols.

Goal (F3 ∧ F1 )%fol = (~(~ ¬ F3 → ¬ F1 ))%fol.

Print F6.

#[local] Unset Printing Notations.
Print F6.

End PrimedSymbols.

Goal forallH 1 (equal (var 1) a ) ≠ forallH 0 (equal (var 0) a ).

Goal apply L a_ Tnil = a.

f a

Goal apply L f_ (Tcons (apply L a_ Tnil ) Tnil ) = f a.

f (f v1)

Goal apply L f_
         (Tcons (apply L f_
                       (Tcons (var 1) Tnil ))
            Tnil ) = (f (f (var 1))).

Definition Ldec : language_decidable L.

Formula_eqdec is opaque !

Check (f a)%fol.

Goal lt_depth L (v #0 = v #1 ∨ exH 2, v #1 = f v #2)%fol
                (v #0 = v #1 ∧ exH 2, v #1 = f v #2)%fol.
Goal lt_depth _ F1 F2.

Check subAllFormula.

Section OnSubstF.
  Let F : Formula L := (exH 2, v #1 ≠ f v #2)%fol.

End OnSubstF.

Example PrfEx1: Prf L [ (A → B → C)%fol] (A → B → C)%fol.

Lemma PrfEx2: Prf L [A → B → C ; A ; A → B ; A ]%fol C.

Print PrfEx2.

Lemma MP' f g H1 H2 H: H = H1 ++ H2 → Prf L H1 (f → g)%fol →
                        Prf L H2 f → Prf L H g.

Cuts the current list of hypotheses as (G++?H), then applies MP

Ltac cutMP G :=
match goal with
|- Prf ?L ?H ?F ⇒ eapply MP' with (H1 := G);
[simpl; reflexivity | try apply AXM | try apply AXM ] end.

Example PrfEx2': Prf L [A → B → C ; A ; A → B ; A ]%fol C. Section ProofOfEx3.

#[local] Arguments MP {L Hyp1 Hyp2 A B} _ _.

Example PrfEx3 : Prf L [] (A → A)%fol.
Print PrfEx3.

End ProofOfEx3.

Rule of contradiction

Example PrfEx4 (A B: Formula L): Prf L [] (¬B → B → A)%fol.

About PrfEx4.

Universal quantifier

Example PrfEx5 : Prf L [] ((allH 1 2, R v #1 v #2) → allH 2, R a v #2)%fol.

Example PrfEx6 : Prf L [] (R v #1 v #1 → allH 0, R v #1 v #1)%fol.

Example PrfContrex7 :
  Prf L [] (R v #1 v #1 → allH 1, R v #1 v #1)%fol.
Example PrfEx8 : Prf L [] ((allH 0, P v #0 → Q v #0) →
                 (allH 0, P v #0) →
                 (allH 0, Q v #0))%fol.

Lemma eq_refl (t:Term L): Prf L nil (t = t)%fol.

About EQ4.
Check @EQ4 L (R_).

Example PrfEx9: Prf L [] (v #0 = v #1 → P v #0 ↔ P v #1)%fol.

Example PrfEx10:
  Prf L [] (v #2 = v #3 → v #0 = v #1 → R v #2 v #0 ↔ R v #3 v #1)%fol.

Example PrfContrex9: Prf L [] (v #1 = v #0 → P v #1 ↔ P v #0)%fol.

Example PrfEx11:
  Prf L [] (v #2 = v #3 → v #0 = v #1 → h v #2 v #0 = h v #3 v #1)%fol.

Lemma ded1: ∀ (A: Formula L), (SysPrf L (Empty_set _) A ) →
                            ∃ pf : Prf L (nil) A , True.

Lemma ded2: SysPrf L (Empty_set _) (A → A)%fol.
Search SysPrf.
Search Add.
Qed.

Lemma ded3 : ∃ pf : Prf L (nil) (A → A)%fol , True.

#[local] Arguments Ensembles.In {_} .
#[local] Arguments Ensembles.Add {_} .
Import Ensembles.

#[local] Hint Unfold mem: sets.

#[local] Hint Resolve In_add1 In_add2: sets.

Fixpoint Adds {A:Type}(X: Ensemble A)(l: list A) :=
  match l with
    nil ⇒ X
  | x::l ⇒ Add (Adds X l) x
  end.

Example SysPrfEx2 : SysPrf L
                      (fun x ⇒ List.In x [A ; A →B ; A → B → C ]%fol)
                      C.

Search SysPrf (?A ∧ ?B)%fol notH.

Search (SysPrf ?L ?T (?A ∧ ?B)%fol → SysPrf ?L ?T ?B).

Search (SysPrf _ _ (¬ ¬ _)%fol).

Search SysPrf (?a = ?b )%fol substF.

Search SysPrf (exH ?v, _)%fol (allH ?v, _)%fol.

Section PeirceProof.
Arguments Add {U}.
Arguments Empty_set {U}.

Definition Peirce : Formula L := (((A → B ) → A ) → A)%fol.

Lemma peirce : SysPrf L Empty_set Peirce.
End PeirceProof.

Section Drinkers_theorem.

Lemma D0 : ∀ i,
      SysPrf _ (Empty_set _)
        ( ¬ forallH i (P (v #i)) → exH i , (¬ (P (v #i))))%fol.

  Lemma D01 T i : SysPrf _ T
                    (¬ forallH i (P (v #i)) →
                      exH i , (¬ (P (v #i))))%fol.

  Let f : Formula L :=
        (exH 0, (P (v #0) → forallH 1 (P (v #1))))%fol.

  Theorem drinkers_thm : SysPrf L (Empty_set _) f.

End Drinkers_theorem.

End Toy.

v1 + 0

Example t1_0: Term LNN :=
apply LNN Plus_
(Tcons (var 1)
(Tcons (apply LNN Zero_ Tnil) Tnil )).
Print t1_0.

forall v0, v0 = 0 \/ exists v1, v0 = S v1

Example f1 : Formula LNN :=
  forallH 0
    (orH (equal (var 0) (apply LNN Zero_ Tnil ))
       (existH 1 (equal (var 0)
                    (apply LNN Succ_
                       (Tcons (var 1) Tnil))))).

Example f2 : Formula LNN :=
  (existH 1 (equal (var 0)
               (apply LNN Succ_
                  (Tcons (var 1) Tnil )))).

Example f3 := (orH (equal (var 0) (apply LNN Zero_ Tnil))
                 (existH 1 (equal (var 0)
                              (apply LNN Succ_
                                 (Tcons (var 1) Tnil))))).