All the declarative tactics now have a more or less bugged implementation.

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 6c31f906a608885f9886e2a22ca22ec196e63840..b177435d4143943e62352bc357d6fc5e918d2e53 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -164,7 +164,7 @@ let tactic_of_ast ast =
   | GrafiteAst.Bydone (_, t) -> Declarative.bydone t 
   | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
      Declarative.we_proceed_by_induction_on t t1
-  | GrafiteAst.Byinduction (_, t, id) -> Declarative.assume id t
+  | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction id t
   | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
   | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) ->
      Declarative.existselim t id1 t1 id2 t2

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 3a24b0d5fd737624da42532c8d4bba173b998f51..50d4be88435e650976eda3fd9052f697bd87e0f1 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -175,11 +175,30 @@ let rewritingstep lhs rhs just conclude =
   ProofEngineTypes.mk_tactic aux
 ;;
 
-let case _ = assert false
+let we_proceed_by_induction_on t pat =
+ (*BUG here: pat unused *)
+ Tactics.elim_intros ~depth:0 t
 ;;
-let thesisbecomes _ = assert false
-;;
-let byinduction _ = assert false
+
+let case id ~params =
+ (*BUG here: id unused*)
+ (*BUG here: it does not verify that the previous branch is closed *)
+ (*BUG here: the params should be parsed telescopically*)
+ (*BUG here: the tactic_terms should be terms*)
+ let rec aux ~params ((proof,goal) as status) =
+  match params with
+     [] -> proof,[goal]
+   | (id,t)::tl ->
+      match ProofEngineTypes.apply_tactic (assume id t) status with
+         proof,[goal] -> aux tl (proof,goal)
+       | _ -> assert false
+ in
+  ProofEngineTypes.mk_tactic (aux ~params)
 ;;
-let we_proceed_by_induction_on _ = assert false
+
+let thesisbecomes t =
+ (*BUG here: nothing done*)
+ Tacticals.id_tac
 ;;
+
+let byinduction t id  = suppose t id None;;

diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma
index e2035d182a11bc87a7bc308e5b4ab18a52ff9cd7..8ff56dde87398e467896aee5d7c3d58b8266e829 100644 (file)
--- a/helm/software/matita/tests/decl.ma
+++ b/helm/software/matita/tests/decl.ma
@@ -97,3 +97,59 @@ obtain (S n) = (S m) by (eq_f ? ? ? ? ? H).
              = n by (sym_eq ? ? ? L)
 done.
 qed.
+
+theorem easy5: ∀n:nat. n*O=O.
+assume n: nat.
+(* Bug here: False should be n*0=0 *)
+we proceed by induction on n to prove False. 
+ case O.
+   the thesis becomes (O*O=O).
+   by (refl_eq ? O) done.
+ case S (m:nat).
+  by induction hypothesis we know (m*O=O) (I).
+  the thesis becomes (S m * O = O).
+  (* Bug here: missing that is equivalent to *)
+  simplify.
+  by I done.
+qed.
+
+inductive tree : Type ≝
+   Empty: tree
+ | Node: tree → tree → tree.
+ 
+let rec size t ≝
+ match t with
+  [ Empty ⇒ O
+  | (Node t1 t2) ⇒ S ((size t1) + (size t2))
+  ].
+  
+theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty. 
+ assume t: tree.
+ suppose (O ≮ O) (trivial).
+ (*Bug here: False should be something else *)
+ we proceed by induction on t to prove False.
+  case Empty.
+    the thesis becomes (O < size Empty → Empty ≠ Empty).
+     suppose (O < size Empty) (absurd).
+     (*Bug here: missing that is equivalent to *)
+     simplify in absurd.
+     (* Here the "natural" language is not natural at all *)
+     we proceed by induction on (trivial absurd) to prove False.
+  (*Bug here: this is what we want
+  case Node (t1:tree) (t2:tree).
+     by induction hypothesis we know (O < size t1 → t1 ≠ Empty) (Ht1).
+     by induction hypothesis we know (O < size t2 → t2 ≠ Empty) (Ht2). *)
+  (*This is the best we can do right now*)
+  case Node.
+   assume t1: tree.
+   by induction hypothesis we know (O < size t1 → t1 ≠ Empty) (Ht1).
+   assume t2: tree.
+   by induction hypothesis we know (O < size t2 → t2 ≠ Empty) (Ht2).
+   suppose (O < size (Node t1 t2)) (Hyp).
+   (*BUG: that is equivalent to missed here *)
+   unfold Not.
+   suppose (Node t1 t2 = Empty) (absurd).
+   (* Discriminate should really generate a theorem to be useful with
+      declarative tactics *)
+   discriminate absurd.
+qed.
\ No newline at end of file