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