Coq lang

prover/build

@@ -36,6 +36,7 @@ other_md_files = [ 'lang/coq-lang.md'
                  , 'strategies/replace-evar-with-func-constant.md'
                  , 'strategies/simplification.md'
                  , 'strategies/search-bound.md'
+                 , 'strategies/typecheck.md'
                  , 'strategies/smt.md'
                  , 'strategies/unfolding.md'
                  , 'utils/load-named.md'

prover/drivers/base.md

@@ -79,6 +79,7 @@ module DRIVER-BASE
   imports STRATEGY-UNFOLDING
   imports STRATEGY-KNASTER-TARSKI
   imports STRATEGY-REPLACE-EVAR-WITH-FUNC-CONSTANT
+  imports STRATEGY-TYPECHECK
   imports SYNTACTIC-MATCH-RULES
   imports VISITOR
   imports PATTERN-LENGTH

prover/drivers/coq-driver.md

@@ -36,8 +36,7 @@ module DRIVER-COQ
        </declarations>
 
 // Add symbol (of sort Term) and equality axiom corresponding to each definition
-  rule Definition ID BINDERs : TYPE1 := TERM (* hasType TYPE2 *) . => Definition ID := TERM (* hasType TYPE2 *) .
-  rule <k> Definition ID := TERM (* hasType TYPE *) .
+  rule <k> Definition ID : TYPE := TERM .
         => .K
            ...
        </k>
@@ -53,7 +52,7 @@ module DRIVER-COQ
              <active> true:Bool </active>
              <parent> .K </parent>
              <claim> \type(CoqIdentToSymbol(ID), CoqTermToPattern(TYPE)) </claim>
-             <strategy> type-check </strategy>
+             <strategy> typecheck </strategy>
              <expected> success </expected>
              <local-context> .Bag </local-context>
              <trace> .K </trace>
@@ -89,7 +88,7 @@ module DRIVER-COQ
   rule CoqTermToPattern(LN:LowerName) => CoqIdentToSymbol(LN)
   rule CoqTermToPattern(#token("Prop", "CoqSort")) => StringToSort("Term")
   rule CoqTermToPattern(fun BINDERs => TERM) => \lambda { CoqBindersToPatterns(BINDERs) } CoqTermToPattern(TERM)
-  rule CoqTermToPattern(forall BINDERs, TERM) => \forall { CoqBindersToPatterns(BINDERs) } CoqTermToPattern(TERM)
+  rule CoqTermToPattern(forall BINDERs, TERM) => \pi { CoqBindersToPatterns(BINDERs) } CoqTermToPattern(TERM)
   rule CoqTermToPattern(match Ts with .CoqEquations end) => \bottom()
   rule CoqTermToPattern(match Ts with (MP:CoqMultPattern => TM:CoqTerm) | EQs end) =>
        \or( #flattenOrs(

prover/lang/coq-lang.md

@@ -101,8 +101,8 @@ module COQ
                        | CoqInductive
   //                   | CoqCoInductive
   syntax CoqSentences ::= List{CoqSentence, ""} [klabel(CoqSentences), format(%1%n%2 %3)]
-  syntax CoqDefinition ::= "Definition" CoqIdent ":=" CoqTerm "(*" "hasType" CoqTerm "*)" "."
-                         | "Definition" CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm "(*" "hasType" CoqTerm "*)" "."
+  syntax CoqDefinition ::= "Definition" CoqIdent ":" CoqTerm ":=" CoqTerm "."
+//                         | "Definition" CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm "."
 
   syntax CoqInductive ::= "Inductive" CoqIndBody "."
   syntax CoqIndBody ::= CoqIdent CoqBinders ":" CoqTerm ":=" CoqIndCases

prover/prover.md

@@ -13,6 +13,7 @@ requires "strategies/intros.k"
 requires "strategies/knaster-tarski.k"
 requires "strategies/matching.k"
 requires "strategies/search-bound.k"
+requires "strategies/typecheck.k"
 requires "strategies/simplification.k"
 requires "strategies/smt.k"
 requires "strategies/reflexivity.k"
@@ -70,7 +71,7 @@ module STRATEGIES-EXPORTED-SYNTAX
                         "in:" AxiomName ","
                         "vars:" VariableNames ","
                         "with:" Patterns ")"
-                    | "type-check"
+                    | "typecheck"
 
   syntax RewriteDirection ::= "->" | "<-"
 

prover/strategies/typecheck.md

@@ -0,0 +1,12 @@
+# typecheck - for Coq terms
+
+```k
+module STRATEGY-TYPECHECK
+  imports PROVER-CORE
+  imports STRATEGIES-EXPORTED-SYNTAX
+
+  rule <strategy> typecheck => noop ...
+       </strategy>
+
+endmodule
+```

prover/t/coq-tests/Logic.v

@@ -7,13 +7,14 @@ Inductive nat : Prop :=
     Z : nat
   | S : (forall (x : nat), nat) .
 
-Definition not := fun (A: Prop) => (forall (x : A), False) (* hasType (forall (x : Prop), Prop) *) .
+Definition not : (forall (x : Prop), Prop) b :=
+  fun (A: Prop) => (forall (x : A), False) .
 
-Definition iff (A B : Prop) : Prop :=
-  (and (forall (x : A), B)) (forall (y : B), A) (* hasType (forall (x : Prop), (forall (y : Prop), Prop)) *) .
+Definition iff : (forall (x : Prop), (forall (y : Prop), Prop)) :=
+  (and (forall (x : A), B)) (forall (y : B), A) .
 
-Definition IF_then_else (P Q R : Prop) : Prop :=
-  (or (and P Q)) (and (not P) R) (* hasType (forall (x : Prop), (forall (y : Prop), (forall (z : Prop), Prop))) *) .
+Definition IF_then_else : (forall (x : Prop), (forall (y : Prop), (forall (z : Prop), Prop))) :=
+  (or (and P Q)) (and (not P) R) .
 
 Inductive ex1 (A : Type) (P : forall (x : A), Prop) : Prop :=
   ex_intro1 : forall (x : A), forall (y : (P x)), ex1 A P .
@@ -27,12 +28,12 @@ Inductive ex2 (A : Type) (P : forall (x : A), Prop) : Prop :=
 Inductive ex4 (A : Type) (P : forall (x : A), Prop) : Prop :=
   ex_intro4 : forall (x : A), forall (y : (P x)), @ ex4 A P .
 
-Definition AndComm :=
+Definition AndComm : (forall (A B : Prop), (forall (c : and A B), and B A)) :=
   fun (A B : Prop) (H : and A B) =>
     match H with
       conj H0 H1 => conj H1 H0
     end
-  (* hasType (forall (A B : Prop), (forall (c : and A B), and B A)) *) .
+  .
 
 // Inductive and (A B : Prop) : Prop :=
 //   conj : forall (x : A), forall (y : B), and A B .

prover/t/coq-tests/nat_ind.v

@@ -6,16 +6,16 @@ Inductive nat : Type :=  Z : nat | S : forall (x : nat), nat .
 
 // axiom \type(Z(), nat())
 
-Definition nat_ind := 
+Definition nat_ind : (forall (P : (forall (x : nat), Prop)),
+                     (forall (y : P 0),
+                     (forall (l : (forall (n : nat),
+                                  (forall (y : P n), P (S n)))),
+                             (forall (n : nat), P n)))) := 
 fun (P : (forall (n : nat), Prop)) (f : P 0) (f0 : forall (n : nat), (forall (x : P n), P (S n))) =>
 fix F (n : nat) := match n with
                            Z => f
                          | S n0 => f0 n0 (F n0)
                    end
-(*
-hasType (forall (P : (forall (x : nat), Prop)),
-        (forall (y : P 0), (forall (l : (forall (n : nat), (forall (y : P n), P (S n)))), (forall (n : nat), P n))))
-*)
 .
 
 // forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n