From 31d3422a07ed889dff7bda3a28884caff30cba07 Mon Sep 17 00:00:00 2001
From: maiorino <??>
Date: Thu, 27 Jul 2006 15:52:31 +0000
Subject: [PATCH] All the declarative tactics now have a more or less bugged
 implementation.

---
 components/grafite_engine/grafiteEngine.ml |  2 +-
 components/tactics/declarative.ml          | 29 +++++++++--
 matita/tests/decl.ma                       | 56 ++++++++++++++++++++++
 3 files changed, 81 insertions(+), 6 deletions(-)

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 6c31f906a..b177435d4 100644
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/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/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 3a24b0d5f..50d4be884 100644
--- a/components/tactics/declarative.ml
+++ b/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/matita/tests/decl.ma b/matita/tests/decl.ma
index e2035d182..8ff56dde8 100644
--- a/matita/tests/decl.ma
+++ b/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
-- 
2.39.2