Apply

lexer.mll

@@ -18,5 +18,6 @@ and token_tactic = parse
   | eof                         { EOF }
   | "intro"                     { INTRO }
   | "assumption"                { ASSUMPTION }
+  | "apply"                     { APPLY }
   | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
   | '.'                         { DOT }

main.ml

@@ -119,6 +119,19 @@ while !subgoals <> [] do
             in
             explore hyps
         )
+      | Apply var -> (
+            let rec explore = function
+              | (var_hyp, TImpl (t1, t2)) :: _ when var_hyp = var && t2 = ty -> (
+                    subgoals := (t1, hyps) :: !subgoals;
+                    fill_holes := function
+                      | hole :: holes -> f ((LApp (LVar var_hyp, hole)) :: holes)
+                      | [] -> fail ()
+                )
+              | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable")
+              | _ :: hyps -> explore hyps
+            in
+            explore hyps;
+        )
 done;
 
 Printf.printf "Final proof :\n%s\n" (string_of_lam (!fill_holes []));;

parser.mly

@@ -10,7 +10,7 @@
 %token <string> VAR_NAME
 %token <string> TYPE_NAME
 
-%token DOT INTRO ASSUMPTION
+%token DOT INTRO ASSUMPTION APPLY
 
 /* L'ordre de définition définit la priorité */
 %right RARROW
@@ -39,3 +39,4 @@ main_tactic:
 tactic:
   | INTRO VAR_NAME DOT                    { Intro $2 }
   | ASSUMPTION DOT                        { Assumption }
+  | APPLY VAR_NAME DOT                    { Apply $2 }

tactic.ml

@@ -2,4 +2,5 @@ open Structs;;
 
 type tactic =
   | Intro of var_lambda
-  | Assumption;;
+  | Assumption
+  | Apply of var_lambda;;