Lemma validate

lib/egraph.ml

@@ -238,7 +238,7 @@ let rec l_of_expr : Ir.expr -> L.t =
         (fun case ->
            let (Ir.Case (pat, _)) = case in
            let pat_vars = Ir.collect_var_in_pat pat in
-           List.is_empty pat_vars)
+           List.is_empty pat_vars && not (pat = Ir.Pat_any))
         case_list
     then (
       let match_list = List.map l_of_expr match_list in

lib/engine.ml

@@ -42,12 +42,15 @@ let make_progress_counter () =
 
 let progress_counter = make_progress_counter ()
 
-let get_proof_of_lemma t =
+let get_proof_of_lemma lemma t =
   let tactic_list = Proof.get_tactic_history t in
   let rec aux tactic_list result =
     match tactic_list with
     | [] -> []
-    | Proof.Assert lemma :: _ -> Proof.Assert lemma :: result
+    | Proof.Assert assertion :: tl ->
+      if assertion = lemma
+      then Proof.Assert assertion :: result
+      else aux tl (Proof.Assert assertion :: result)
     | hd :: tl -> aux tl (hd :: result)
   in
   aux (List.rev tactic_list) []
@@ -73,44 +76,130 @@ let is_lhs lemma =
   | _ -> false
 ;;
 
+let count_tale_rewrite tactics =
+  let rec count_tale_rewrite tactics =
+    match tactics with
+    | hd :: tl ->
+      (match hd with
+       | Proof.RewriteInAt _ | Proof.RewriteReverse _ -> 1 + count_tale_rewrite tl
+       | _ -> 1)
+    | [] -> 1
+  in
+  count_tale_rewrite (List.rev tactics)
+;;
+
+let get_previous_state (t : Prover.proof_node) statelist =
+  let prev_tactics = Proof.get_tactic_history t.t in
+  let index = count_tale_rewrite prev_tactics in
+  let rec get_previous_state (t : Prover.proof_node) statelist i =
+    match i with
+    | 1 -> [ t ]
+    | _ ->
+      let parent_id = t.parent in
+      let parent_node = Prover.ProofSet.find parent_id statelist in
+      t :: get_previous_state parent_node statelist (i - 1)
+  in
+  get_previous_state t statelist index
+;;
+
+let apply_and_get_lemmas (new_t : Prover.proof_node) assert_list (work : Prover.workelt) =
+  match assert_list with
+  | [] ->
+    let prev_lemma_list = Proof.get_lemma_stack work.t.t in
+    let new_lemma_list = Proof.get_lemma_stack work.next_t.t in
+    let assert_list =
+      List.filter (fun x -> not (List.mem x prev_lemma_list)) new_lemma_list
+    in
+    new_t, Proof.SimplIn "goal", -1., assert_list |> List.map snd
+  | _ ->
+    let new_env = List.filter (fun x -> not (List.mem x work.next_t.t.env)) new_t.t.env in
+    (match new_env with
+     | [] ->
+       let heads, tl = split_tale assert_list in
+       let new_t =
+         List.fold_left
+           (fun t lemma -> Prover.just_apply_tactic t (Proof.Assert lemma))
+           new_t
+           heads
+       in
+       let _ = print_endline "Lemma List" in
+       let _ = assert_list |> List.iter (fun x -> Proof.pp_prop x |> print_endline) in
+       let _ = print_endline "End of Lemma List" in
+       new_t, Proof.mk_assert tl, 0., assert_list
+     | _ ->
+       let _ = print_endline "New Env" in
+       let _ = new_env |> Ir.pp_t |> print_endline in
+       let _ = print_endline "Lemma List" in
+       let _ = assert_list |> List.iter (fun x -> Proof.pp_prop x |> print_endline) in
+       let _ = print_endline "End of Lemma List" in
+       let heads, tl = split_tale assert_list in
+       let new_t =
+         List.fold_left
+           (fun t lemma ->
+              let t = Prover.just_apply_tactic t (Proof.Assert lemma) in
+              Prover.just_apply_tactic ~is_lhs:(Some (is_lhs lemma)) t Proof.Reflexivity)
+           new_t
+           heads
+       in
+       new_t, Proof.mk_assert tl, 0., assert_list)
+;;
+
 let rec progress worklist statelist lemma_set =
   match Prover.WorkList.is_empty worklist with
   | true -> failwith "worklist is empty"
   | false ->
     let prev_worklist, work = Prover.WorkList.take_exn worklist in
-    let t, tactic, next_t, r, _ = work in
     let _ = print_endline "=================================================" in
     let i = progress_counter () in
     let _ = print_endline ("Progress: " ^ string_of_int i) in
-    let _ = Proof.pp_t t |> print_endline in
+    let _ = Proof.pp_t work.t.t |> print_endline in
     let _ =
-      print_endline (">>> " ^ Proof.pp_tactic tactic ^ "(rank : " ^ string_of_int r ^ ")")
-    in
-    let _ = Proof.pp_t next_t |> print_endline in
-    (* let _ = if i = 5 then Proof.proof_top next_t in *)
-    let lemma_set =
-      match is_end_of_conj t next_t with
-      | true ->
-        let lemma_list = Proof.get_lemma_stack next_t in
-        let lemma = List.hd (List.rev lemma_list) |> snd in
-        let tactics = get_proof_of_lemma next_t in
-        let original_goal = get_conj_goal t in
-        let lemma_set = Prover.LemmaSet.add (original_goal, lemma, tactics) lemma_set in
-        lemma_set
-      | false -> lemma_set
+      print_endline
+        (">>> "
+         ^ Proof.pp_tactic work.tactic
+         ^ "(rank : "
+         ^ string_of_float work.rank
+         ^ ")")
     in
-    (match next_t.proof with
+    let _ = Proof.pp_t work.next_t.t |> print_endline in
+    (* let _ = if i = 12 then Proof.proof_top work.next_t.t in *)
+    (match work.next_t.t.proof with
      | _, [], proof -> Prover.ProofSet.empty, Some proof
      | _ ->
+       let lemma_set =
+         match is_end_of_conj work.t.t work.next_t.t with
+         | true ->
+           let lemma_list = Proof.get_lemma_stack work.next_t.t in
+           let lemma = List.hd (List.rev lemma_list) |> snd in
+           let tactics = get_proof_of_lemma lemma work.next_t.t in
+           let original_goal = get_conj_goal work.next_t.t in
+           let _ = print_endline "original goal" in
+           let _ = original_goal |> Proof.pp_prop |> print_endline in
+           let _ = print_endline "lemma" in
+           let _ = lemma |> Proof.pp_prop |> print_endline in
+           let _ = print_endline "tactics" in
+           let _ =
+             tactics |> List.iter (fun tactic -> Proof.pp_tactic tactic |> print_endline)
+           in
+           let lemma_set =
+             Prover.LemmaSet.add { original_goal; lemma; tactics } lemma_set
+           in
+           lemma_set
+         | false -> lemma_set
+       in
        let prev_worklist =
-         match tactic with
+         match work.tactic with
          | Proof.Reflexivity | Proof.Discriminate ->
-           Prover.deduplicate_worklist prev_worklist next_t
+           Prover.deduplicate_worklist prev_worklist work.next_t.t
          | _ -> prev_worklist
        in
-       let tactic_list = Prover.mk_candidates next_t in
-       let worklist, statelist =
-         Prover.prune_rank_worklist_update_state_list next_t tactic_list statelist
+       let tactic_list = Prover.mk_candidates work.next_t.t in
+       let worklist, statelist, is_stuck =
+         Prover.prune_rank_worklist_update_state_list
+           work.next_t
+           tactic_list
+           statelist
+           lemma_set
        in
        let _ =
          print_endline
@@ -119,62 +208,53 @@ let rec progress worklist statelist lemma_set =
        in
        let _ =
          Prover.WorkList.iter
-           (fun (_, tactic, _, r, _) ->
-              Proof.pp_tactic tactic ^ "(rank:" ^ string_of_int r ^ ")" |> print_endline)
+           (fun elt ->
+              Proof.pp_tactic elt.tactic ^ "(rank:" ^ string_of_float elt.rank ^ ")"
+              |> print_endline)
            worklist
        in
-       if Prover.is_stuck worklist
-       then (
-         let t_lemma = Finder.make_lemmas_by_advanced_generalize next_t lemma_set in
-         match t_lemma with
-         | Some (new_t, assert_list) ->
-           let new_t, tactic, r, assert_list =
-             match assert_list with
-             | [] ->
-               let prev_lemma_list = Proof.get_lemma_stack t in
-               let new_lemma_list = Proof.get_lemma_stack new_t in
-               let assert_list =
-                 List.filter (fun x -> not (List.mem x prev_lemma_list)) new_lemma_list
-               in
-               new_t, Proof.SimplIn "goal", -1, assert_list |> List.map snd
-             | _ ->
-               let new_env =
-                 List.filter (fun x -> not (List.mem x next_t.env)) new_t.env
-               in
-               let _ = print_endline "New Env" in
-               let _ = new_env |> Ir.pp_t |> print_endline in
-               let _ = print_endline "Lemma List" in
-               let _ =
-                 assert_list |> List.iter (fun x -> Proof.pp_prop x |> print_endline)
-               in
-               let _ = print_endline "End of Lemma List" in
-               let heads, tl = split_tale assert_list in
-               let new_t =
-                 List.fold_left
-                   (fun t lemma ->
-                      let t = Proof.apply_assert lemma t in
-                      Proof.apply_tactic ~is_lhs:(Some (is_lhs lemma)) t Proof.Reflexivity)
-                   new_t
-                   heads
-               in
-               new_t, Proof.mk_assert tl, 0, assert_list
-           in
-           let _ = new_t |> Proof.pp_t |> print_endline in
-           let original_goal = get_conj_goal next_t in
-           let lemma_set =
-             Prover.LemmaSet.add_list
-               lemma_set
-               (List.map (fun lemma -> original_goal, lemma, []) assert_list)
-           in
-           let new_state = Proof.apply_tactic new_t tactic in
-           progress
-             (Prover.WorkList.add
-                prev_worklist
-                (new_t, tactic, new_state, r, Prover.order_counter ()))
-             (Prover.ProofSet.add new_state statelist)
-             lemma_set
-         | None -> progress prev_worklist statelist lemma_set)
-       else progress (Prover.WorkList.merge prev_worklist worklist) statelist lemma_set)
+       (match is_stuck with
+        | true ->
+          let previous_states = get_previous_state work.next_t statelist in
+          let t_lemmas_list = Finder.find_lemma previous_states lemma_set in
+          let new_worklist, new_state_list, new_lemma_set =
+            List.fold_left
+              (fun (worklist, statelist, lemma_set) (new_t, assert_list) ->
+                 let new_t, tactic, r, assert_list =
+                   apply_and_get_lemmas new_t assert_list work
+                 in
+                 let _ = new_t.t |> Proof.pp_t |> print_endline in
+                 let original_goal = get_conj_goal work.next_t.t in
+                 let lemma_set =
+                   Prover.LemmaSet.add_list
+                     lemma_set
+                     (List.map
+                        (fun lemma ->
+                           let lemma = Proof.make_lemma_consistent lemma in
+                           Prover.{ original_goal; lemma; tactics = [] })
+                        assert_list)
+                 in
+                 let new_state = Prover.just_apply_tactic new_t tactic in
+                 let new_state_list =
+                   Prover.ProofSet.add new_state.id new_state statelist
+                 in
+                 let new_worklist =
+                   Prover.WorkList.add
+                     worklist
+                     { t = new_t
+                     ; tactic
+                     ; next_t = new_state
+                     ; rank = r
+                     ; order = Prover.order_counter ()
+                     }
+                 in
+                 new_worklist, new_state_list, lemma_set)
+              (prev_worklist, statelist, lemma_set)
+              t_lemmas_list
+          in
+          progress new_worklist new_state_list new_lemma_set
+        | false ->
+          progress (Prover.WorkList.merge prev_worklist worklist) statelist lemma_set))
 ;;
 
 let proof_auto definition axiom program_a program_b goal =
@@ -188,10 +268,18 @@ let proof_auto definition axiom program_a program_b goal =
   let axiom = axiom |> axiom_to_prop env in
   let init_t = Proof.create_t env ~proof:(axiom, [], []) () in
   let first_assertion = Proof.parse_tactic init_t goal in
-  let next_t = Proof.apply_tactic init_t first_assertion in
+  let id = Prover.get_id () in
+  let (init_t : Prover.proof_node) = Prover.{ t = init_t; id; parent = -1 } in
+  let next_t = Prover.just_apply_tactic init_t first_assertion in
   let worklist =
     Prover.WorkList.of_list
-      [ init_t, first_assertion, next_t, 0, Prover.order_counter () ]
+      [ { t = init_t
+        ; tactic = first_assertion
+        ; next_t
+        ; rank = 0.
+        ; order = Prover.order_counter ()
+        }
+      ]
   in
   match progress worklist Prover.ProofSet.empty Prover.LemmaSet.empty with
   | _, Some proof ->