apply généralisé

proof.ml

@@ -192,7 +192,27 @@ let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof =
     Some (new_h, new_t, cs), gs
 
 let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
-  let rec get_hyp = function
+  let rec is_implied (goal_ty : ty) (t : ty) : bool =
+    match t with
+    t when t = goal_ty -> true
+    | Arr (_, t2) -> is_implied goal_ty t2
+    | _ -> false
+  in
+  let rec generate_goals (goal_ty : ty) (t : ty) (cs : context)
+  (h' : hlam) (h : hlam) (gs : goal list) : proof =
+    match t with
+    Arr (t1, t2) when t2 = goal_ty ->
+      let new_h = Ref (ref Hole) in
+      fill h (HApp (h', new_h));
+      Some (new_h, t1, cs), gs
+    | Arr (t1, t2) ->
+      let new_h = Ref (ref Hole) in
+      let _ = fill h (HApp (h', new_h)) in
+      let gs = (new_h, t1, cs) :: gs in
+      generate_goals goal_ty t2 cs h' new_h gs
+    | _ -> failwith "cannot happen"
+  in
+  let rec get_hyp : context -> (hlam * ty) = function
     [] -> raise (TacticFailed "no such hypothesis in context")
     | (hyp_id', _, h', t') :: _ when hyp_id = hyp_id' -> (h', t')
     | _ :: cs -> get_hyp cs
@@ -201,13 +221,9 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
   None -> raise (TacticFailed "no current goal")
   | Some (h, goal_ty, cs) ->
     let h', t' = get_hyp cs in
-    match t' with
+    if is_implied goal_ty t'
-    Arr (t1, t2) when t2 = goal_ty ->
+    then generate_goals goal_ty t' cs h' h gs
-      let new_h = Ref (ref Hole) in
+    else raise (TacticFailed "not an implication")
-      fill h (HApp (h', new_h));
-      Some (new_h, t1, cs), gs
-    | Arr _ -> (* failwith "wrong types" *) (g, gs)
-    | _ -> (* failwith "expected ->" *) (g, gs)
 
 let tact_intros : proof -> proof =
   let rec push (p : proof) =