Library hydras.MoreAck.LNN_Examples

From Coq Require Import Arith Lists.List.
Require Import fol folProp Languages LNN folProof.
Import FolNotations.
Import NNnotations.

Section bare_syntax.

Definition f0 : Formula LNN :=
      forallH 0
        (orH
           (equal (var 0) Zero)
           (existH 1 (equal (var 0)
                          (apply
                             (Languages.Succ_ : Functions LNN)
                             (Tcons (var 1) (@Tnil _)))))).

Import LNN.
Print f0.
Check Zero.
Set Printing All.
Unset Printing All.

Print f0.
End bare_syntax.

Print f0.
Goal f0 = (allH 0, v#0 = Zero ∨ exH 1, v#0 = Succ v#1)%fol.

Locate Plus.
Locate "_ + _".
 Example t1_0 : Term _ := Plus (S_ (var 1))%fol Zero.
Print t1_0.
Check S_ Zero.

Print t1_0.

Section Examples.

Let t1: Term LNN := Plus (var 1) Zero.

Let f1 : Formula LNN :=
  (forallH 0
    (v#0 = Zero ∨
          existH 1 (v#0 = Succ (v#1))))%fol.
Print f1.



Print Relations.

Let f2 : Formula LNN :=
   (existH 2 (LT Zero (v#2) ∧ natToTerm 4 = Plus (v#2) (v#2)))%fol.

Let f2' : Formula LNN :=
   (existH 2 (Zero < v#2 ∧ natToTerm 4 = Plus (v#2) (v#2)))%fol.

Let f3 := (v#0 = Zero ∨ existH 1 (v#0 = Succ (v#1)))%fol.

Let f4 := (v#0 = v#1 + v#1 ↔ v#0 = v#1 × (natToTerm 2))%fol.

Print f4.

Check (Plus Zero Zero)%fol.






Locate LT.

End Examples.





Check GEN LNN nil (v#0 = v#0)%fol 1.




Goal Prf LNN nil
         (forallH 0 (v#0 = v#0))%fol →
       Prf LNN nil (Zero = Zero)%fol.