Correct lambdapi proofs when an epsilon-term is read on the input

Note: need a new proof rule in Zenon.Main, basically the epsilon axiom.

Author: gburel

dkterm.ml

@@ -26,6 +26,7 @@ type dkterm =
   | Dktrue                                     (* true *)
   | Dkfalse                                    (* false *)
   | Dkequal       of dkterm * dkterm * dkterm  (* equal type*term*term *)
+  | Dkeps         of dkterm                    (* epsilon prop *)
 
   | DkRfalse        of dkterm
   | DkRnottrue      of dkterm
@@ -53,6 +54,7 @@ type dkterm =
   | DkRsubst        of dkterm * dkterm * dkterm * dkterm * dkterm * dkterm * dkterm
   | DkRconglr       of dkterm * dkterm * dkterm * dkterm * dkterm * dkterm * dkterm
   | DkRcongrl       of dkterm * dkterm * dkterm * dkterm * dkterm * dkterm * dkterm
+  | DkReps          of dkterm * dkterm * dkterm * dkterm
 ;;
 
 type line =
@@ -116,6 +118,7 @@ let mk_existstype (t)          = Dkexiststype t
 let mk_true                    = Dktrue
 let mk_false                   = Dkfalse
 let mk_equal      (t1, t2, t3) = Dkequal (t1, t2, t3)
+let mk_eps  (t) = Dkeps t
 
 let mk_DkRfalse        (pr)                      = DkRfalse (pr)
 let mk_DkRnottrue      (pr)                      = DkRnottrue (pr)
@@ -143,6 +146,7 @@ let mk_DkRnotalltype   (p, pr1, pr2)             = DkRnotalltype (p, pr1, pr2)
 let mk_DkRsubst        (a, p, t1, t2, pr1, pr2, pr3)  = DkRsubst (a, p, t1, t2, pr1, pr2, pr3)
 let mk_DkRconglr       (a, p, t1, t2, pr1, pr2, pr3)  = DkRconglr (a, p, t1, t2, pr1, pr2, pr3)
 let mk_DkRcongrl       (a, p, t1, t2, pr1, pr2, pr3)  = DkRcongrl (a, p, t1, t2, pr1, pr2, pr3)
+let mk_DkReps          (a, p, pr1, pr2)  = DkReps (a, p, pr1, pr2)
 
 let mk_decl       (v, t)       = Dkdecl (v, t)
 let mk_rwrt       (l, t1, t2)  = Dkrwrt (l, t1, t2)

dkterm.mli

@@ -28,7 +28,7 @@ type dkterm =
   | Dktrue                                     (* true *)
   | Dkfalse                                    (* false *)
   | Dkequal       of dkterm * dkterm * dkterm  (* equal type*term*term *)
-
+  | Dkeps         of dkterm                    (* epsilon prop *)
   | DkRfalse        of dkterm
   | DkRnottrue      of dkterm
   | DkRaxiom        of dkterm * dkterm * dkterm
@@ -55,6 +55,7 @@ type dkterm =
   | DkRsubst        of dkterm * dkterm * dkterm * dkterm * dkterm * dkterm * dkterm
   | DkRconglr       of dkterm * dkterm * dkterm * dkterm * dkterm * dkterm * dkterm
   | DkRcongrl       of dkterm * dkterm * dkterm * dkterm * dkterm * dkterm * dkterm
+  | DkReps          of dkterm * dkterm * dkterm * dkterm (* type, predicate, proof of eps, proof of ex *)
 
 type line =
   | Dkdecl of var * dkterm                     (* declaration of symbols *)
@@ -86,6 +87,7 @@ val mk_existstype       : dkterm -> dkterm
 val mk_true             : dkterm
 val mk_false            : dkterm
 val mk_equal            : dkterm * dkterm * dkterm -> dkterm
+val mk_eps       : dkterm -> dkterm
 
 val mk_DkRfalse         : dkterm -> dkterm
 val mk_DkRnottrue       : dkterm -> dkterm
@@ -113,6 +115,7 @@ val mk_DkRnotalltype    : dkterm * dkterm * dkterm -> dkterm
 val mk_DkRsubst         : dkterm * dkterm * dkterm * dkterm * dkterm * dkterm * dkterm -> dkterm
 val mk_DkRconglr        : dkterm * dkterm * dkterm * dkterm * dkterm * dkterm * dkterm -> dkterm
 val mk_DkRcongrl        : dkterm * dkterm * dkterm * dkterm * dkterm * dkterm * dkterm -> dkterm
+val mk_DkReps            : dkterm * dkterm * dkterm * dkterm -> dkterm
 
 val mk_decl             : var * dkterm -> line
 val mk_rwrt             : dkterm list * dkterm * dkterm -> line

globals.ml

@@ -47,3 +47,5 @@ let end_comment() =
   else "*)"
 
 let has_a_conjecture = ref true
+
+let epsilon_on_input = ref false

globals.mli

@@ -41,3 +41,5 @@ val end_comment : unit -> string;;
 
 (* Has a conjecture, useful for SZS output *)
 val has_a_conjecture : bool ref;;
+
+val epsilon_on_input : bool ref (* has an epsilon-term been read on the input? *)

lltolp.ml

@@ -206,10 +206,16 @@ and translate_expr e =
      let p' = translate_expr p in
      mk_exists (ty, mk_lam (nv, p'))
   | Eex _ -> assert false
-  | Etau _ as e ->
-     let v = Index.make_tau_name e in
-     let ty = translate_type (get_type e) in
-     mk_var (v, ty)
+  | Etau (Evar (v, _) as v', p, _) ->
+     if !Globals.epsilon_on_input then
+       let ty = translate_type (get_type v') in
+       let nv = mk_var (v, ty) in
+       let p' = translate_expr p in
+       mk_eps (mk_lam (nv, p'))
+     else
+       let v = Index.make_tau_name e in
+       let ty = translate_type (get_type e) in
+       mk_var (v, ty)
   | Elam (Evar (v, _) as v', p, _) ->
      let ty = translate_type (get_type v') in
      let nv = mk_var (v, ty) in
@@ -531,9 +537,13 @@ let rec trproof_dk p =
 	  let pzz = substitute [(vx, zz)] px in
 	  let prpzz = mk_pr_var pzz in
 	  let sub = trproof_dk (List.nth phyps 0) in
-	  let lam = mk_lam (dkzz, mk_lam (prpzz, sub)) in
 	  let conc = get_pr_var exp in
-	  mk_DkRex (a, dkp, lam, conc)
+	  if !Globals.epsilon_on_input then
+            let lam = mk_lam (prpzz, sub) in
+	    mk_DkReps (a, dkp, lam, conc)
+          else
+            let lam = mk_lam (dkzz, mk_lam (prpzz, sub)) in
+            mk_DkRex (a, dkp, lam, conc)
      | Rall (Eall (Evar (_, _) as vx, px, _) as allp, t) ->
 	if (is_binder_of_type_var allp) then
 	  let dkp = translate_quant_to_dklam allp in

lpprint.ml

@@ -171,6 +171,7 @@ and print_dk_term_aux o (t, var_context) =
      fprintf o "(%a) = (%a)"
 	     print_dk_term_aux (t2, var_context)
 	     print_dk_term_aux (t3, var_context)
+  | Dkeps t -> fprintf o "ε (%a)" print_dk_term_aux (t, var_context)
   | DkRfalse (pr) -> fprintf o "Rfalse\n (%a)" print_dk_term_aux (pr, var_context)
   | DkRnottrue (pr) -> fprintf o "Rnottrue\n (%a)" print_dk_term_aux (pr, var_context)
   | DkRaxiom (p, pr1, pr2) ->
@@ -328,6 +329,12 @@ and print_dk_term_aux o (t, var_context) =
 	     print_dk_term_aux (pr1, var_context)
 	     print_dk_term_aux (pr2, var_context)
 	     print_dk_term_aux (pr3, var_context)
+  | DkReps (a, p, pr1, pr2) ->
+     fprintf o "Reps\n (%a)\n (%a)\n (%a)\n (%a)\n"
+       print_dk_zentype_aux (a, var_context)
+       print_dk_term_aux (p, var_context)
+       print_dk_term_aux (pr1, var_context)
+       print_dk_term_aux (pr2, var_context)
   | _ -> assert false
  and print_dk_term o t = print_dk_term_aux o (t, [])
 

parsetptp.mly

@@ -168,7 +168,8 @@ expr:
   | expr EQSYM expr                    { eeq $1 $3 }
   | expr NEQSYM expr                   { enot (eeq $1 $3) }
   | OPEN expr CLOSE                    { $2 }
-  | HASH LBRACKET var_list RBRACKET COLON unit_formula { etau (List.hd $3, $6) }
+  | HASH LBRACKET var_list RBRACKET COLON unit_formula { Globals.epsilon_on_input := true;
+                                                         etau (List.hd $3, $6) }
 ;
 arguments:
   | OPEN expr_list CLOSE         { $2 }