The Coq mailing list

["Alfonso Nishikawa" <alfonso.nishikawa AT gmail.com>]

Hi!
I'm a beginner and I have been trying to proof:

[code]
Require Import ListSet.
Variable A:Set.
Variable T:Set.

Axiom eq_dec_T:forall(tf1 tf2:T),{tf1=tf2}+{~tf1=tf2}.

Lemma a : forall (a:T) (x:set T), ~ set_In a (set_remove eq_dec_T a x).
[/code]

Until I realized it can't be proved because it's not true nor false. So I thought about other goal, prove this:

[code]
Variable a : T.
Variable x : set T.
Axiom anbx : ~ set_In a x.
Definition x1 := set_add eq_dec_T a x : set T.

Lemma aaa : ~ set_In a (set_remove eq_dec_T a x1).
  unfold set_remove.
[/code]

and I get this:

================
~ set_In a
  ((fix set_remove (a : T) (x : set T) {struct x} : set T :=
      match x with
      | List.nil => empty_set T
      | List.cons a1 x1 =>
          if eq_dec_T a a1 then x1 else List.cons a1 (set_remove a x1)
      end) a x1)

-------------------------------------------------------------
Why can't I do this: get 2 new subgoals with parameters 'a' and 'x1' subsituted in the function 'fix....' ?
If I could, I would have:

=================
~ set_In a (empy_set T)

--- and 

=================
~ set_In a (eq_dec_T a a then x1 ...

and that is trivial...

In this second problem I had to put parameters as Variable's, Axiom and Definition because I have problems putting them as -> -> -> ¿how can I put then in that way?

If someone can help me I will be very grateful.