lean2/tests/lean/tactic2.lean

38 lines
891 B
Text
Raw Normal View History

(** import("tactic.lua") **)
Variables p q r : Bool
Theorem T1 : p => q => p /\ q :=
Discharge (fun H1,
Discharge (fun H2,
let H1 : p := _,
H2 : q := _
in Conj H1 H2
)).
exact (* solve first metavar *)
done
exact (* solve second metavar *)
done
(**
simple_tac = Repeat(imp_tac() ^ conj_tac() ^ assumption_tac())
**)
Theorem T2 : p => q => p /\ q /\ p := _.
simple_tac
done
Show Environment 1
Theorem T3 : p => p /\ q => r => q /\ r /\ p := _.
(** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **)
done
(* Display proof term generated by previous tac *)
Show Environment 1
Theorem T4 : p => p /\ q => r => q /\ r /\ p := _.
Repeat (OrElse (apply Discharge) (apply Conj) conj_hyp exact)
done
(* Display proof term generated by previous tac *)
Show Environment 1