arithm example

examples/logic/Arithm.gf

@@ -0,0 +1,64 @@
+abstract Arithm = Logic ** {
+
+-- arithmetic
+fun 
+  Nat, Real  : Dom ;
+data
+  Zero : Elem Nat ;
+  Succ : Elem Nat -> Elem Nat ;
+fun
+  trunc : Elem Real -> Elem Nat ;
+
+  EqNat : (m,n : Elem Nat) -> Prop ;
+  LtNat : (m,n : Elem Nat) -> Prop ;
+  Div   : (m,n : Elem Nat) -> Prop ;
+  Even  : Elem Nat -> Prop ;
+  Odd   : Elem Nat -> Prop ;
+  Prime : Elem Nat -> Prop ;
+
+  one  : Elem Nat ;
+  two  : Elem Nat ;
+  sum  : (m,n : Elem Nat) -> Elem Nat ;
+  prod : (m,n : Elem Nat) -> Elem Nat ;
+data
+  evax1 : Proof (Even Zero) ;
+  evax2 : (n : Elem Nat) -> Proof (Even n) -> Proof (Odd (Succ n)) ;
+  evax3 : (n : Elem Nat) -> Proof (Odd n)  -> Proof (Even (Succ n)) ;
+  eqax1 : Proof (EqNat Zero Zero) ;
+  eqax2 : (m,n : Elem Nat) -> Proof (EqNat m n) -> Proof (EqNat (Succ m) (Succ n)) ;
+fun
+  IndNat : (C : Elem Nat -> Prop) -> 
+             Proof (C Zero) -> 
+             ((x : Elem Nat) -> Hypo (C x) -> Proof (C (Succ x))) -> 
+                Proof (Univ Nat C) ;
+
+def 
+  one = Succ Zero ;
+  two = Succ one ;
+  sum m (Succ n) = Succ (sum m n) ;
+  sum m Zero = m ;
+  prod m (Succ n) = sum (prod m n) m ;
+  prod m Zero = Zero ;
+  LtNat m n = Exist Nat (\x -> EqNat n (sum m (Succ x))) ;
+  Div m n = Exist Nat (\x -> EqNat m (prod x n)) ;
+  Prime n = Conj 
+              (LtNat one n) 
+              (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
+
+fun ex1 : Text ;
+def ex1 = 
+  ThmWithProof 
+    (Univ Nat (\x -> Disj (Even x) (Odd x))) 
+    (IndNat 
+       (\x -> Disj (Even x) (Odd x)) 
+       (DisjIl (Even Zero) (Odd Zero) evax1) 
+       (\x -> \h -> DisjE (Even x) (Odd x) (Disj (Even (Succ x)) (Odd (Succ x))) 
+         (Hypoth (Disj (Even x) (Odd x)) h) 
+         (\a -> DisjIr (Even (Succ x)) (Odd (Succ x)) 
+            (evax2 x (Hypoth (Even x) a))) 
+         (\b -> DisjIl (Even (Succ x)) (Odd (Succ x)) 
+            (evax3 x (Hypoth (Odd x) b))
+         )
+       )
+     ) ;
+} ;

examples/logic/ArithmEng.gf

@@ -0,0 +1,61 @@
+--# -path=.:mathematical:present:resource-1.0/api:prelude
+
+concrete ArithmEng of Arithm = LogicEng ** 
+  open
+    GrammarEng,
+    ParadigmsEng,
+    ProoftextEng,
+    MathematicalEng,
+    CombinatorsEng,
+    ConstructorsEng
+  in { 
+
+lin
+  Nat  = UseN  (regN "number") ;
+  Zero = UsePN (regPN "zero") ;
+  Succ = appN2 (regN2 "successor") ;
+
+  EqNat x y = mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) x y) ;
+--  LtNat = adj2 ["smaller than"] ;
+--  Div   = adj2 ["divisible by"] ;
+  Even  x = mkS (predA (regA "even") x) ;
+  Odd   x = mkS (predA (regA "odd") x) ;
+  Prime x = mkS (predA (regA "prime") x) ;
+
+  one = UsePN (regPN "one") ;
+  two = UsePN (regPN "two") ;
+  sum = appColl (regN2 "sum") ;
+  prod = appColl (regN2 "product") ;
+
+  evax1 = 
+    proof (by (ref (mkLabel ["the first axiom of evenness ,"]))) 
+      (mkS (pred (regA "even") (UsePN (regPN "zero")))) ;
+  evax2 n c = 
+    appendText c 
+      (proof (by (ref (mkLabel ["the second axiom of evenness ,"]))) 
+      (mkS (pred (regA "odd") (appN2 (regN2 "successor") (UsePN (regPN "zero")))))) ;
+  evax3 n c = 
+    appendText c 
+      (proof (by (ref (mkLabel ["the third axiom of evenness ,"]))) 
+      (mkS (pred (regA "even") (appN2 (regN2 "successor") (UsePN (regPN "zero")))))) ;
+
+{-
+
+  eqax1 = ss ["by the first axiom of equality , zero is equal to zero"] ;
+  eqax2 m n c = {s = 
+    c.s ++ ["by the second axiom of equality , the successor of"] ++ m.s ++ 
+    ["is equal to the successor of"] ++ n.s} ;
+-}
+
+  IndNat C d e = {s = 
+    ["we proceed by induction . for the basis ,"] ++ d.s ++ 
+    ["for the induction step, consider a number"] ++ C.$0 ++ 
+    ["and assume"] ++ C.s ++ 
+    --- "(" ++ e.$1 ++ ")" ++ 
+    "." ++ e.s ++ 
+    ["hence , for all numbers"] ++ C.$0 ++ "," ++ C.s ; lock_Text = <>} ;
+
+  ex1 = proof ["the first theorem and its proof"] ;
+
+} ;
+

examples/logic/LogicI.gf

@@ -4,7 +4,8 @@ incomplete concrete LogicI of Logic =
     Prooftext, 
     Grammar, 
     Constructors, 
-    Combinators 
+    Combinators,
+    ParamX ---
   in {
 
 lincat 
@@ -24,7 +25,10 @@ lin
   Abs = mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
 
   Univ A B = 
-    mkS (mkAdv for_Prep (mkNP all_Predet (mkNP (mkDet IndefArt (mkCN A $0))))) B ;
+    AdvS 
+      (mkAdv for_Prep (mkNP all_Predet 
+        (mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0)))))
+      B ;
 
   DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
   DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ;
@@ -46,4 +50,8 @@ lin
   Hypoth A h = proof hypothesis A ;
 
 
+--- this should not be here, but is needed for variables
+lindef
+  Elem s = {s = \\_ => s ; a = {n = Sg ; p = P3} ; lock_NP = <>} ;
+
 }

lib/resource-1.0/Makefile

@@ -12,7 +12,7 @@ GFCP=$(GFC) -preproc=./mkPresent
 
 .PHONY: show-path all test alltenses pretest langs present mathematical multimodal compiled treebank stat gfdoc clean
 
-all: show-path present alltenses langs multimodal mathematical compiled
+all: show-path present alltenses mathematical multimodal compiled langs
 
 show-path:
 	@echo GF_LIB_PATH=$(GF_LIB_PATH)