The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

On Fri, Jul 10, 2015 at 01:04:22PM +0200, Emilio Jesús Gallego Arias wrote:
> Abhishek Anand 
> <abhishek.anand.iitg AT gmail.com>
>  writes:
> 
> > I don't know about merlin, but you can use Ltac pattern matching and "type
> > of" to conveniently find out types of sub-expressions.
> 
> I have also found quite useful ssreflect's
> 
> "set f := pattern"
> 
> tactic to find out types of tricky sub-expressions; the matching
> mechanism usually works well for my full-of-holes patterns.
> 
> I don't know if this can be done with the standard Coq tactics.

Coq standard "set" supports patterns. In Kenneth's example you can
do for instance:

Fixpoint evenb n :=
  match n with
  | O => true
  | S 0 => false
  | S (S n) => evenb n
  end.

Theorem even_n__oddb_Sn : forall n : nat,
 evenb n = negb (evenb (S n)).
Fixpoint f (n0 : nat) := (match n0 with
| 0 => false
| S n' => evenb n'
end).
Proof.
intros; elim n; intros; simpl in |- *; auto. rewrite H . simpl in |- *.
assert (neg_neg: negb (negb (f n)) = f n).
elim f. simpl. reflexivity. simpl. reflexivity.
set (a:= match _ with 0 => _ | _ => _ end).
(* 
a = negb (negb a)
*)

or even directly

destruct (match _ with 0 => _ | _ => _ end).
(*
 2 subgoals
  
  n, n0 : nat
  H : evenb n0 = negb (evenb (S n0))
  neg_neg : negb (negb (f n)) = f n
  ============================
   true = negb (negb true)

subgoal 2 is:
 false = negb (negb false)
*)

Best,

Hugo Herbelin