Elim

lexer.mll

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

main.ml

@@ -132,6 +132,16 @@ while !subgoals <> [] do
             in
             explore hyps;
         )
+      | Elim var -> (
+            let rec explore = function
+              | (var_hyp, ty_hyp) :: _ when var_hyp = var && ty_hyp = TFalse -> (
+                    fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
+                )
+              | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable")
+              | _ :: hyps -> explore hyps
+            in
+            explore hyps;
+        )
 done;
 
 let finalLam = !fill_holes [] in

parser.mly

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

tactic.ml

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