From 9d5de2f3f3a8921397b939ce2143b22aa71959ea Mon Sep 17 00:00:00 2001
From: maiorino <??>
Date: Thu, 27 Jul 2006 16:45:53 +0000
Subject: [PATCH] Automation enabled for declarative proofs. Cool.

---
 components/grafite_engine/grafiteEngine.ml |  8 +--
 components/tactics/declarative.ml          | 65 ++++++++++++----------
 components/tactics/declarative.mli         | 10 ++--
 matita/tests/decl.ma                       | 50 +++++++++++++++++
 4 files changed, 95 insertions(+), 38 deletions(-)

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index b177435d4..031832232 100644
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -158,20 +158,20 @@ let tactic_of_ast ast =
   | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
   | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
   | GrafiteAst.By_term_we_proved (_, t, ty, id, t1) ->
-     Declarative.by_term_we_proved t ty id t1
+     Declarative.by_term_we_proved ~dbd:(LibraryDb.instance()) t ty id t1
   | GrafiteAst.We_need_to_prove (_, t, id, t2) ->
      Declarative.we_need_to_prove t id t2
-  | GrafiteAst.Bydone (_, t) -> Declarative.bydone t 
+  | GrafiteAst.Bydone (_, t) -> Declarative.bydone ~dbd:(LibraryDb.instance()) t
   | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
      Declarative.we_proceed_by_induction_on t t1
-  | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction id t
+  | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id
   | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
   | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) ->
      Declarative.existselim t id1 t1 id2 t2
   | GrafiteAst.Case (_,id,params) -> Declarative.case id params
   | GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2
   | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
-     Declarative.rewritingstep termine t1 t2 cont
+     Declarative.rewritingstep ~dbd:(LibraryDb.instance ()) termine t1 t2 cont
 
 let classify_tactic tactic = 
   match tactic with
diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 370e326db..4a7d3e52c 100644
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -45,30 +45,33 @@ let suppose t id ty =
       (fun _ metasenv ugraph -> ty,metasenv,ugraph))
 ;;
 
-let by_term_we_proved t ty id ty' =
- match t with
-    None -> assert false
-  | Some t ->
-     let continuation =
-      match ty' with
-         None -> Tacticals.id_tac
-       | Some ty' ->
-          Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
-	   (fun _ metasenv ugraph -> ty,metasenv,ugraph)
-     in
-      Tacticals.thens
-      ~start:
-        (Tactics.cut ty
-          ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
-      ~continuations:
-        [ continuation ; Tactics.apply t ]
+let by_term_we_proved ~dbd t ty id ty' =
+ let just =
+  match t with
+     None -> Tactics.auto ~dbd ~params:[]
+   | Some t -> Tactics.apply t
+ in
+  let continuation =
+   match ty' with
+      None -> Tacticals.id_tac
+    | Some ty' ->
+       Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+        (fun _ metasenv ugraph -> ty,metasenv,ugraph)
+  in
+   Tacticals.thens
+   ~start:
+     (Tactics.cut ty
+       ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
+   ~continuations:[ continuation ; just ]
 ;;
 
-let bydone t =
-   match t with
-    None -> assert false
-  | Some t ->
-    (Tactics.apply ~term:t)
+let bydone ~dbd t =
+ let just =
+  match t with
+     None -> Tactics.auto ~dbd ~params:[]
+   | Some t -> Tactics.apply t
+ in
+  just
 ;;
 
 let we_need_to_prove t id ty =
@@ -111,13 +114,13 @@ let existselim t id1 t1 id2 t2 =
 
 let andelim = existselim;;
 
-let rewritingstep lhs rhs just conclude =
+let rewritingstep ~dbd lhs rhs just conclude =
  let aux ((proof,goal) as status) =
   let (curi,metasenv,proofbo,proofty) = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let eq,trans =
    match LibraryObjects.eq_URI () with
-      None -> assert false (*TODO*)
+      None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
     | Some uri ->
       Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
   in
@@ -125,8 +128,10 @@ let rewritingstep lhs rhs just conclude =
    CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
   let just =
    match just with
-      None -> assert false (*TOOD*)
-    | Some just -> just
+      None ->
+       Tactics.auto ~dbd
+        ~params:["paramodulation","on"; "timeout","3"]
+    | Some just -> Tactics.apply just
   in
    match lhs with
       None ->
@@ -151,7 +156,7 @@ let rewritingstep lhs rhs just conclude =
                 ~continuations:
                   [ Tactics.apply prhs ;
                     Tactics.apply (Cic.Rel 1) ;
-                    Tactics.apply just]) status
+                    just]) status
           | Some name ->
              let mk_fresh_name_callback =
 	      fun metasenv context _ ~typ ->
@@ -169,11 +174,11 @@ let rewritingstep lhs rhs just conclude =
                       ~continuations:
                         [ Tactics.apply prhs ;
                           Tactics.apply (Cic.Rel 1) ;
-                          Tactics.apply just]
+                          just]
                    ]) status)
     | Some lhs ->
        match conclude with
-          None -> ProofEngineTypes.apply_tactic (Tactics.apply just) status
+          None -> ProofEngineTypes.apply_tactic just status
         | Some name ->
             let mk_fresh_name_callback =
 	     fun metasenv context _ ~typ ->
@@ -185,7 +190,7 @@ let rewritingstep lhs rhs just conclude =
                 ~start:
                   (Tactics.cut ~mk_fresh_name_callback
                     (Cic.Appl [eq ; ty ; lhs ; rhs]))
-                ~continuations:[ Tacticals.id_tac ; Tactics.apply just ]) status
+                ~continuations:[ Tacticals.id_tac ; just ]) status
  in
   ProofEngineTypes.mk_tactic aux
 ;;
diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli
index 6e3a7b696..e5a8a590c 100644
--- a/components/tactics/declarative.mli
+++ b/components/tactics/declarative.mli
@@ -27,9 +27,11 @@ val assume : string -> Cic.term -> ProofEngineTypes.tactic
 
 val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
 
-val by_term_we_proved : Cic.term option -> Cic.term -> string -> Cic.term option ->ProofEngineTypes.tactic
+val by_term_we_proved :
+ dbd:HMysql.dbd -> Cic.term option -> Cic.term -> string -> Cic.term option ->
+  ProofEngineTypes.tactic
 
-val bydone : Cic.term option -> ProofEngineTypes.tactic
+val bydone : dbd:HMysql.dbd -> Cic.term option -> ProofEngineTypes.tactic
 
 val we_need_to_prove :
  Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
@@ -49,5 +51,5 @@ val andelim :
  Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
 
 val rewritingstep :
- Cic.term option -> Cic.term -> Cic.term option -> Cic.name option ->
-  ProofEngineTypes.tactic
+ dbd:HMysql.dbd -> Cic.term option -> Cic.term -> Cic.term option ->
+  Cic.name option -> ProofEngineTypes.tactic
diff --git a/matita/tests/decl.ma b/matita/tests/decl.ma
index 4359b4a9d..a0d3a0bd6 100644
--- a/matita/tests/decl.ma
+++ b/matita/tests/decl.ma
@@ -72,6 +72,43 @@ theorem easy2: ∀n,m. n * m = O → n = O ∨ m = O.
   ]
 qed.
 
+theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O.
+ assume n: nat.
+ assume m: nat.
+ (* base case *)
+ by _ we proved (O = O) (trivial).
+ by _ we proved (O = O ∨ m = O) (trivial2).
+ by _ we proved (O*m=O → O=O ∨ m=O) (base_case).
+ (* inductive case *)
+ we need to prove
+  (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
+  (inductive_case).
+   assume n1: nat.
+   suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
+   (* base case *)
+   by _ we proved (S n1 = O ∨ O = O) (pre_base_case2).
+   by _ we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
+   (* inductive case *)
+   we need to prove
+    (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
+      (S n1 * S m1 = O → S n1 = O ∨ S m1 = O)) (inductive_hyp2).
+     assume m1: nat.
+     suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
+     suppose (S n1 * S m1 = O) (absurd_hyp).
+     simplify in absurd_hyp.
+     by _ we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+     (* BUG: automation failure *)
+     by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
+     (* BUG: automation failure *)
+     by (False_ind ? the_absurd)
+   done.
+   (* the induction *)
+   by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
+ done.
+ (* the induction *)
+ by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
+done.
+qed.
 
 theorem easy3: ∀A:Prop. (A ∧ ∃n:nat.n ≠ n) → True.
  assume P: Prop.
@@ -98,6 +135,19 @@ obtain (S n) = (S m) by (eq_f ? ? ? ? ? H).
 done.
 qed.
 
+theorem easy45: ∀n,m,p. n = m → S m = S p → n = S p → S n = n.
+assume n: nat.
+assume m:nat.
+assume p:nat.
+suppose (n=m) (H).
+suppose (S m = S p) (K).
+suppose (n = S p) (L).
+obtain (S n) = (S m) by _.
+             = (S p) by _.
+             = n by _
+done.
+qed.
+
 theorem easy5: ∀n:nat. n*O=O.
 assume n: nat.
 (* Bug here: False should be n*0=0 *)
-- 
2.39.2