The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Dear Saulo,

All beginners are a little bit confused because Boolean values
are claimed to be related to truth. But just consider them as values,
say colors and
  if objEq obj obj' then true else containsObj objs obj'
as syntactic sugar for
  match objColor obj obj' with
    | blue -> blue 
    | red -> containsObj objs obj'
  end
Let us call E this expression.
If E = red, then objColor obj obj' = red.
Then you'll agree that, in order to prove it, you need to consider
the possible values for (objColor obj obj') in order to get the result
of the computation. 
One of the 2 cases happens to produce a particular hypothesis, 
namely blue = red. So what? It turns out to be the equality 
you want to prove. 
(Moreover it is easy to prove any equality from blue = red, 
or from 3 = 25, just by Leibniz rule).

JF

On Thu, Dec 18, 2014 at 03:43:33PM -0300, Saulo Araujo wrote:
>    Dear Jean-Francois,
>    Thanks for your help. I believe that in some moment I got close to your
>    proof of the second theorem. Probably I got confused when I saw true =
>    false as a hypothesis :)
>    In a informal setting, I believe one would probably say that if 
>    (if objEq obj obj' then true else containsObj objs obj') = false
>    then objEq obj obj' = false /\ containsObj objs obj' = false
>    But after the reply of Andrew and yours I got the impression that Coq
>    forces us to deal with "impossible" cases. 
>    Thanks again,
>    Saulo
>    On Thu, Dec 18, 2014 at 2:18 PM, Jean-Francois Monin
>    
> <[1]jean-francois.monin AT imag.fr>
>  wrote:
> 
>      No need for inversion in the second theorem :
>      true = false |- true = false
>      holds just by assumption (or trivial).
>       Theorem containsObj_t2 :
>         forall (obj obj' : OBJ) (objs : list OBJ),
>         containsObj (obj :: objs) obj' = false -> objEq obj obj' =  false.
>       Proof.
>         intros * e.
>         simpl in e.
>         destruct (objEq obj obj').
>           trivial.
>           trivial.
>      Qed.
> 
>      No need for inversion in the first theorem as well :
>      after an additional destruct (containsObj objs obj'), you get the same
>      situation.
>       Theorem containsObj_t1 :
>         forall (obj obj' : OBJ) (objs : list OBJ),
>         containsObj (obj :: objs) obj' = false -> containsObj objs obj' = 
>      false.
>       Proof.
>         intros * e.
>         simpl in e.
>         destruct (objEq obj obj').
>           destruct (containsObj objs obj').
>             trivial.
>             trivial.
>           trivial.
>      Qed.
> 
>      More generally, looking at "small inversions" in the litterature
>      may provide you simple intuitions on what inversion means.
> 
>      JFM
>      On Thu, Dec 18, 2014 at 10:51:55AM -0600, Andrew Hirsch 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
>      
> <[1][2]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
>      
> <[2][3]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
>      >        
> <[3][4]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"
>      
> <[4][5]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
>      >
> 
>      --
>      Jean-Francois Monin
>