The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 08/29/2013 02:57 AM, Ryan Wisnesky wrote:
> I'm mechanizing some meta-theory, and need to prove around a dozen lemmas 
> that state that various pieces of syntax cannot appear inside themselves.  
> The basic cases are easy, but the more complicated cases are giving me 
> trouble, so I'd like to appeal to this list for help.  Here is an example:
>
> Inductive ty : Set :=
>   | one : ty
>   | prop : ty
>   | prod : ty ->  ty ->  ty
>   | pow : ty ->  ty
>   | dom : ty
>   | zero : ty
>   | sum : ty ->  ty ->  ty.
>
> (* easy *)
> Lemma contra_sum : forall t t', t = sum t t' ->  False.
> Proof.
>   intros. induction t; intros; try discriminate.
>   apply IHt1. injection H. intros. subst t2.
>   auto.
> Qed.
The typical solution is to define a size function, and use automation to 
solve equalities on nats, for example the omega tactic.

Fixpoint ty_len (t : ty) : nat :=
  match t with
  | one => 0
  | prop => 0
  | prod t1 t2 => S (ty_len t1 + ty_len t2)
  | pow t => S (ty_len t)
  | dom => 0
  | zero => 0
  | sum t1 t2 => S (ty_len t1 + ty_len t2)
  end.

Lemma contra_sum_prod : forall t1 t0 t2,
                   (t0 = sum (prod t1 t0) t2) -> False.
Proof.
  intros t1 t0 t2 H.
  apply (f_equal ty_len) in H; simpl in H; omega.
Qed.