The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi Andrew,

It works indeed. I got a little confused after so many Coq hours :)

Thanks a lot!

Saulo

On Thu, Dec 18, 2014 at 1:51 PM, Andrew Hirsch <akhirsch AT cs.cornell.edu> wrote:

The same trick seems to work for me. I get two goals, true = false (with H : true = false, inversion H), and false = false (trivial). Here's the script I have:

Theorem containsObj_t2 : 

  forall (obj obj' : OBJ) (objs : list OBJ),

  containsObj (obj :: objs) obj' = false ->

  objEq obj obj' = false.

Proof.

  intros; simpl in H.

  destruct (objEq obj obj').

  inversion H.

  trivial.

Qed.

On Thu, Dec 18, 2014 at 10:23 AM, Saulo Araujo <saulo2 AT gmail.com> wrote:

Andrew,

Maybe you could help me with this another very simple theorem:

Theorem containsObj_t2 :

  forall (obj obj' : OBJ) (objs : list OBJ), 

  containsObj (obj :: objs) obj' = false -> objEq obj obj' = false.

Proof.

  intros.

  simpl in H.

Qed.

Just like in the other theorem, Coq says that  H is

 (if objEq obj obj' then true else containsObj objs obj') = false

Again, I think is safe to say that objEq obj obj' = false but I cannot convince Coq about that. I tried destruct and inversion as in your last suggestion but this time it does not do the tricky. Sorry about asking such beginner questions but I am really stuck,

Thanks in advance,

Saulo

On Thu, Dec 18, 2014 at 1:05 PM, Saulo Araujo <saulo2 AT gmail.com> wrote:

Thans a lot Andrew. It works :

Theorem containsObj_t1 :

  forall (obj obj' : OBJ) (objs : list OBJ), 

  containsObj (obj :: objs) obj' = false -> containsObj objs obj' = false.

Proof.

  intros.

  simpl in H.

  destruct (objEq obj obj').

  inversion H.

  trivial.

Qed.

Now I am going to try to understand what inversion does. Thanks a lot!

On Thu, Dec 18, 2014 at 12:57 PM, Andrew Hirsch <akhirsch AT cs.cornell.edu> wrote:

Try destruct objEq obj obj'. Then you should get two goals, one where H has type true = false (which you can then invert) and one where H had the type of the goal.

-akh

On Dec 18, 2014 9:47 AM, "Saulo Araujo" <saulo2 AT gmail.com> wrote:

Hi,

I am trying to prove the following very simple theorem:

Require Import Arith.

Require Import List. Import ListNotations.

Inductive OBJ := Obj : nat -> OBJ.

Definition objEq obj obj' := let 'Obj id := obj 

  in let 'Obj id' := obj' 

  in beq_nat id id'.

Fixpoint containsObj objs obj := match objs with

    | [] => false

    | obj' :: objs' => if objEq obj' obj then true else containsObj objs' obj

  end.

Theorem containsObj_t1 :

  forall (obj obj' : OBJ) (objs : list OBJ), 

  containsObj (obj :: objs) obj' = false -> containsObj objs obj' = false.

When I try

Proof.

  intros.

  simpl in H.

Qed.

Coq shows that H is

(if objEq obj obj' then true else containsObj objs obj') = false

From where I believe it is safe to say that containsObj objs obj' = false. 

But no matter what I try, I cannot convince Coq that containsObj objs obj' = false :)

Any suggestions?

Thanks in advance,

Saulo