On pattern matching in Ltac
Consider the following development:
Require Import Arith.
Require Import Compare_dec.
Definition max (n p:nat) : nat :=
if le_lt_dec n p then p else n.
Lemma le_max_eq : forall n p, n <= p -> p = max n p.
intros n p; unfold max; case (le_lt_dec n p);simpl.
trivial.
intros; apply le_antisym;auto with arith.
Qed.
Ltac max_le_rw H :=
match goal with H : ?a <= ?b |- ?G => elim (le_max_eq a b H) end.
Lemma L1: forall n p, n <= p -> max n p + max n p = 2 * p.
intros n p H; max_le_rw H.
simpl;auto.
Qed.
(* seems OK,
but ... *)
Lemma L2 : forall n p, n <= p -> 2 <= 3 -> max n p + max n p = 2 * p.
intros n p H H0.
max_le_rw H.
(*
n : nat
p : nat
H : n <= p
H0 : 2 <= 3
============================
max n p + max n p = 2 * p
*)
What does this example show about pattern matching in Ltac?
Define a tactic similar to max_le_rw (using elim), which works fine on L2.
Hint: You may use "type of" in your tactic.
Solution
Look at this file
Going home
Pierre Castéran