instrument choose (#29)

README.md

@@ -254,22 +254,22 @@ Multi-threaded translation to Lambdapi (with `mk 7`):
   * term abbrevs: 700 Mo
   * Unfortunately, Lambdapi is too slow and takes too much memory to be able to check so big files on my laptop. It can however check some prefix of `hol.ml` (see below).
 
-Multi-threaded translation to Dedukti (with `mk 7`):
-  * dk file generation time: 9m19s
+Multi-threaded translation to Dedukti:
+  * dk file generation time: 9m19s (with `mk 7`) 8m56s (with `mk 21`)
   * dk file size: 3.7 Go
   * type abbrevs: 652 Ko
   * term abbrevs: 731 Mo
   * kocheck can check it in 12m52s
   * dkcheck is unable to check the generated dk file on my laptop for lack of memory (I have only 32 Go RAM and the process is stopped after 11m16s)
 
 Results for `hol.ml` up to `arith.ml`:
-  * proof dumping time: 13s 101 Mo
-  * number of proof steps: 409 K
-  * dk file generation: 21s 97 Mo
-  * checking time with dk check: 26s
-  * checking time with kocheck -j 7: 16s
-  * lp file generation: 15s 70 Mo (4s with `mk 7`)
-  * checking time with lambdapi: 1m54s (2m with `mk 7`)
+  * proof dumping time: 13s 100 Mo
+  * number of proof steps: 405 K
+  * dk file generation: 20s 96 Mo
+  * checking time with dk check: 19s
+  * checking time with kocheck -j 7: 14s
+  * lp file generation: 15s 69 Mo (4s with `mk 7`)
+  * checking time with lambdapi: 1m53s (2m with `mk 7`)
   * translation to Coq: 10s
   * checking time for Coq: 7m5s (with `mk 22` and `j 7`)
 

bool.ml

@@ -359,6 +359,8 @@ Q0*)
 let SIMPLE_EXISTS v th =
   EXISTS (mk_exists(v,concl th),v) th;;
 
+(*Q0
+(*REMOVE [v], [th1: Γ₁ ⊢ ? abs], [th2: Γ₂ ⊢ c₂] ~~> [Γ₁ U Γ₂ - {abs v} ⊢ c₂] *)
 let CHOOSE =
   let P = `P:A->bool` and Q = `Q:bool` in
   let pth =
@@ -376,7 +378,7 @@ let CHOOSE =
         let th5 = PINST [snd(dest_var v),aty] [abs,P; concl th2,Q] pth in
         MP (MP th5 th4) th1
     with Failure _ -> failwith "CHOOSE";;
-
+Q0*)
 let SIMPLE_CHOOSE v th =
   CHOOSE(v,ASSUME (mk_exists(v,hd(hyp th)))) th;;
 

fusion.ml

@@ -48,6 +48,7 @@ module type Hol_kernel =
       | Pspec of term * int
       | Pgen of term * int
       | Pexists of term * term * int
+      | Pchoose of term * int * int
       | Pdisj1 of term * int
       | Pdisj2 of term * int
       | Pdisj_cases of int * int * int
@@ -123,6 +124,7 @@ module type Hol_kernel =
       val SPEC : term -> thm -> thm
       val GEN : term -> thm -> thm
       val EXISTS : term * term -> thm -> thm
+      val CHOOSE : (term * thm) -> thm -> thm
       val DISJ1 : thm -> term -> thm
       val DISJ2 : term -> thm -> thm
       val DISJ_CASES : thm -> thm -> thm -> thm
@@ -189,6 +191,7 @@ module Hol : Hol_kernel = struct
   | Pspec of term * int
   | Pgen of term * int
   | Pexists of term * term * int
+  | Pchoose of term * int * int
   | Pdisj1 of term * int
   | Pdisj2 of term * int
   | Pdisj_cases of int * int * int
@@ -751,6 +754,15 @@ module Hol : Hol_kernel = struct
     | _ -> failwith "GEN"
   ;;
 
+  let CHOOSE (v,Sequent(asl1,c1,k1)) (Sequent(asl2,c2,k2)) =
+    match c1 with
+    | Comb(Const("?",_),(Abs(bv,bod) as p)) ->
+      let asl2 = term_remove (mk_comb(p,v)) asl2 in
+      let asl2 = term_remove (vsubst [v,bv] bod) asl2 in
+      new_theorem (term_union asl1 asl2) c2 (Pchoose(v,k1,k2))
+    | _ -> failwith "CHOOSE"
+  ;;
+
   let DISJ1 (Sequent(asl,c,k)) p =
     new_theorem asl (Comb(Comb(cst_disj,c),p)) (Pdisj1(p,k));;
 

theory_hol.lp

@@ -47,7 +47,7 @@ symbol ∧ᵢ [p : El bool] : Prf p → Π [q : El bool], Prf q → Prf (∧ p q
 symbol ∧ₑ₁ [p q : El bool] : Prf (∧ p q) → Prf p;
 symbol ∧ₑ₂ [p q : El bool] : Prf (∧ p q) → Prf q;
 symbol ∃ᵢ [a] (p : El a → El bool) t : Prf (p t) → Prf (∃ p);
-symbol ∃ₑ [a] p : Prf (∃ p) → Π r, (Π x:El a, Prf (p x) → Prf r) → Prf r;
+symbol ∃ₑ [a p] : Prf (∃ (λ x, p x)) → Π [r], (Π x:El a, Prf (p x) → Prf r) → Prf r;
 symbol ∨ᵢ₁ [p : El bool] : Prf p → Π q : El bool, Prf (∨ p q);
 symbol ∨ᵢ₂ (p : El bool) [q : El bool] : Prf q → Prf (∨ p q);
 symbol ∨ₑ [p q : El bool] :

xdk.ml

@@ -508,6 +508,20 @@ let proof tvs rmap =
        out oc "or_elim %a %a %a %a (h0 : Prf %a => %a) (h0 : Prf %a => %a)"
          term l term r (sub k1) p1 term (concl th2)
          term l (sub k2) p2 term r sub_at k3
+    | Pchoose(v,k1,k2) ->
+       let p1 = proof_at k1 in
+       let Proof(th1,_) = p1 in
+       let p2 = proof_at k2 in
+       let Proof(th2,_) = p2 in
+       begin match concl th1 with
+       | Comb(_,p) ->
+          let rmap' = add_var rmap v in
+          out oc "ex_elim %a %a %a %a (%a => h0 : Prf(%a %a) => %a)"
+            typ (type_of v) term p (sub k1) p1 term (concl th2)
+            (decl_var tvs rmap') v term p (var rmap') v
+            (subproof tvs rmap' [] [] ts k2) p2
+       | _ -> assert false
+       end
   in proof
 ;;
 
@@ -519,7 +533,7 @@ let typ_arity oc k =
   for i = 1 to k do out oc "%a -> " typ_name "Set" done; typ_name oc "Set";;
 
 let decl_typ oc (n,k) =
-  out oc "%a : %a.\n" name n typ_arity k;;
+  out oc "%a : %a.\n" typ_name n typ_arity k;;
 
 let decl_typ_param tvs oc b = out oc "%a : %a -> " (typ tvs) b typ_name "Set";;
 

xlib.ml

@@ -393,7 +393,7 @@ let deps (Proof(_,content)) =
   match content with
   | Pdisj_cases(k1,k2,k3) -> [k1;k2;k3]
   | Ptrans(k1,k2) | Pmkcomb(k1,k2) | Peqmp(k1,k2) | Pdeduct(k1,k2)
-  | Pconj(k1,k2) | Pmp(k1,k2)
+  | Pconj(k1,k2) | Pmp(k1,k2) | Pchoose(_,k1,k2)
     -> [k1;k2]
   | Pabs(k,_) | Pinst(k,_) | Pinstt(k,_)| Pdeft(k,_,_,_)
   | Pconjunct1 k | Pconjunct2 k | Pdisch(_,k) | Pspec(_,k) | Pgen(_,k)
@@ -430,6 +430,7 @@ let code_of_proof (Proof(_,c)) =
   | Pdisj1 _ -> 22
   | Pdisj2 _ -> 23
   | Pdisj_cases _ -> 24
+  | Pchoose _ -> 25
 ;;
 
 let name_of_code = function
@@ -458,10 +459,11 @@ let name_of_code = function
   | 22 -> "disj1"
   | 23 -> "disj2"
   | 24 -> "disj_cases"
+  | 25 -> "choose"
   | _ -> assert false
 ;;
 
-let nb_rules = 25;;
+let nb_rules = 26;;
 
 (* [count_thm uses p] updates [uses] with the dependencies of [p]. *)
 let count_thm (uses : int array) (p : proof) : unit =

xlp.ml

@@ -386,6 +386,17 @@ let proof tvs rmap =
        let l,r = binop_args (concl th1) in
        out oc "∨ₑ %a (λ h0 : Prf %a, %a) (λ h0 : Prf %a, %a)"
          (sub k1) p1 term l sub_at k2 term r sub_at k3
+    | Pchoose(v,k1,k2) ->
+       let p1 = proof_at k1 in
+       let Proof(th1,_) = p1 in
+       begin match concl th1 with
+       | Comb(_,p) ->
+          let rmap' = add_var rmap v in
+          out oc "∃ₑ %a (λ %a, λ h0 : Prf(%a %a), %a)"
+            (sub k1) p1 (decl_var rmap') v term p (var rmap') v
+            (subproof tvs rmap' [] [] ts k2) (proof_at k2)
+       | _ -> assert false
+       end
   in proof
 ;;
 
@@ -638,7 +649,8 @@ symbol ∧ᵢ [p q] : Prf p → Prf q → Prf (∧ p q);
 symbol ∧ₑ₁ [p q] : Prf (∧ p q) → Prf p;
 symbol ∧ₑ₂ [p q] : Prf (∧ p q) → Prf q;
 symbol ∃ᵢ [a] p (t : El a) : Prf (p t) → Prf (∃ p);
-symbol ∃ₑ [a] p : Prf (∃ p) → Π r, (Π x:El a, Prf (p x) → Prf r) → Prf r;
+symbol ∃ₑ [a p] :
+  Prf (∃ (λ x:El a, p x)) → Π [r], (Π x:El a, Prf (p x) → Prf r) → Prf r;
 symbol ∨ᵢ₁ [p] : Prf p → Π q, Prf (∨ p q);
 symbol ∨ᵢ₂ p [q] : Prf q → Prf (∨ p q);
 symbol ∨ₑ [p q] :