The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

Works great, thanks!

On Aug 29, 2013, at 4:13 AM, Robbert Krebbers 
<mailinglists AT robbertkrebbers.nl>
 wrote:

> 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.