Library Waterproof.Tactics.Induction
Require Import Ltac2.Ltac2.
Require Import Ltac2.Message.
Local Ltac2 concat_list (ls : message list) : message :=
List.fold_right concat (of_string "") ls.
Require Import Util.Binders.
Require Import Util.Constr.
Require Import Util.Evars.
Require Import Util.Goals.
Require Import Util.Hypothesis.
Require Import Util.MessagesToUser.
Require Import Notations.Sets.
Lemma Sn_eq_nplus1 : forall n, S n = n + 1.
Proof.
intro n.
induction n.
reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed.
Open Scope subset_scope.
The induction principle we would like to use
with sealed notations.
Lemma induction_principle_elements {P : nat -> Prop} :
P 0 -> (∀ k ∈ nat, P k -> P (k + 1)) ->
∀ k ∈ nat, P k.
Proof.
intros H_base IH k k_in_nat.
induction k as [| k IHk].
- exact H_base.
- rewrite Sn_eq_nplus1.
apply IH.
+ exact I.
+ apply IHk.
exact I.
Qed.
P 0 -> (∀ k ∈ nat, P k -> P (k + 1)) ->
∀ k ∈ nat, P k.
Proof.
intros H_base IH k k_in_nat.
induction k as [| k IHk].
- exact H_base.
- rewrite Sn_eq_nplus1.
apply IH.
+ exact I.
+ apply IHk.
exact I.
Qed.
induction_without_hypothesis_naming
Performs mathematical induction.- x: ident, the variable to perform the induction on.
- performs induction on x.
- If x is a natural number, the first goal is wrapped in NaturalInduction.Base.Wrapper and the second goal is wrapped in NaturalInduction.Step.Wrapper.
- Otherwise, the resulting cases are wrapped in the StateGoal.Wrapper.
Ltac2 induction_without_hypothesis_naming (x: ident) :=
lazy_match! Control.goal () with
| ∀ _ ∈ conv nat, _ =>
check_binder_warn (Control.goal ()) x true;
apply induction_principle_elements;
Control.focus 1 1 (fun () => apply NaturalInduction.Base.unwrap);
Control.focus 2 2 (fun () =>
let stmt :=
change_binder_name_under_seal (Control.goal ()) x in
change $stmt;
apply NaturalInduction.Step.unwrap)
| forall _ : nat, _ =>
check_binder_warn (Control.goal ()) x true;
intro $x;
let x_hyp := Control.hyp x in
let ih_x := Fresh.in_goal @_IH in
induction $x_hyp as [| $x $ih_x];
Control.focus 1 1 (fun () =>
apply NaturalInduction.Base.unwrap);
Control.focus 2 2 (fun () =>
rewrite Sn_eq_nplus1;
revert $ih_x;
revert $x;
apply NaturalInduction.Step.unwrap)
| _ =>
throw (of_string "Cannot apply natural induction on this goal.")
end.
Local Ltac2 panic_ident_Qed (i : ident) :=
if Ident.equal i @Qed
then throw (of_string "Syntax error: variable name expected after 'on'.")
else ().
Ltac2 Notation "We" "use" "induction" "on" x(ident) :=
panic_ident_Qed (x);
panic_if_goal_wrapped ();
induction_without_hypothesis_naming x.
lazy_match! Control.goal () with
| ∀ _ ∈ conv nat, _ =>
check_binder_warn (Control.goal ()) x true;
apply induction_principle_elements;
Control.focus 1 1 (fun () => apply NaturalInduction.Base.unwrap);
Control.focus 2 2 (fun () =>
let stmt :=
change_binder_name_under_seal (Control.goal ()) x in
change $stmt;
apply NaturalInduction.Step.unwrap)
| forall _ : nat, _ =>
check_binder_warn (Control.goal ()) x true;
intro $x;
let x_hyp := Control.hyp x in
let ih_x := Fresh.in_goal @_IH in
induction $x_hyp as [| $x $ih_x];
Control.focus 1 1 (fun () =>
apply NaturalInduction.Base.unwrap);
Control.focus 2 2 (fun () =>
rewrite Sn_eq_nplus1;
revert $ih_x;
revert $x;
apply NaturalInduction.Step.unwrap)
| _ =>
throw (of_string "Cannot apply natural induction on this goal.")
end.
Local Ltac2 panic_ident_Qed (i : ident) :=
if Ident.equal i @Qed
then throw (of_string "Syntax error: variable name expected after 'on'.")
else ().
Ltac2 Notation "We" "use" "induction" "on" x(ident) :=
panic_ident_Qed (x);
panic_if_goal_wrapped ();
induction_without_hypothesis_naming x.
*
Removes the NaturalInduction.Base.Wrapper.
Arguments:
Does:
Raises fatal exceptions:
- t : constr, goal that is wrapped
- removes the NaturalInduction.Base.Wrapper from the goal
- If the goal is the type t wrapped in the base case wrapper, i.e. the goal is not of the form NaturalInduction.Base.Wrapper t.
Ltac2 base_case (t:constr) :=
lazy_match! goal with
| [|- NaturalInduction.Base.Wrapper ?v] =>
match Constr.equal v t with
| true => apply (NaturalInduction.Base.wrap)
| false => throw (of_string "Wrong goal specified.")
end
| [|- _] => throw (of_string "No need to indicate showing a base case.")
end.
Ltac2 Notation "We" "first" "show" "the" "base" "case" t(constr) := base_case t.
lazy_match! goal with
| [|- NaturalInduction.Base.Wrapper ?v] =>
match Constr.equal v t with
| true => apply (NaturalInduction.Base.wrap)
| false => throw (of_string "Wrong goal specified.")
end
| [|- _] => throw (of_string "No need to indicate showing a base case.")
end.
Ltac2 Notation "We" "first" "show" "the" "base" "case" t(constr) := base_case t.
*
Removes the NaturalInduction.Step.Wrapper.
Arguments: none
Does:
Raises fatal exceptions:
- removes the NaturalInduction.Step.Wrapper from the goal
- If the goal is not wrapped in the induction step case wrapper, i.e. the goal is not of the form NaturalInduction.Step.Wrapper G for some type G.
Ltac2 induction_step () :=
lazy_match! goal with
| [|- NaturalInduction.Step.Wrapper _] => apply (NaturalInduction.Step.wrap)
| [|- _] => throw (of_string "No need to indicate showing an induction step.")
end.
Ltac2 Notation "We" "now" "show" "the" "induction" "step" := induction_step ().
lazy_match! goal with
| [|- NaturalInduction.Step.Wrapper _] => apply (NaturalInduction.Step.wrap)
| [|- _] => throw (of_string "No need to indicate showing an induction step.")
end.
Ltac2 Notation "We" "now" "show" "the" "induction" "step" := induction_step ().