The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

If you want a simple argument that it is not the case in general, simply consider:

isFree(x)  := a=x

Then

a:constraint

b:constraint

H:a=a
-------------

a=b

has no proof unless you know that a=b.

If you have a doubt on a general statement (here, ∀ (constraint:Type) (isFree:constraint→Prop) a b, isFree a → isFree b),
instantiate some universally quantified variables with the most constrained interesting structures.

Here "constraint" must have at least 2 inhabitants (a and b), so take bool for instance, and set 'a' to be "true".

Then, simply try to see if there could be an instance of "isFree" such that "isFree true" holds, but not "isFree b" for any 'b'.

Such "isFree" exists (isFree x := true=x), thus your statement does not hold.

2015-07-22 8:24 GMT+02:00 Bahman Sistany <bsistany AT yahoo.ca>:

Hi,

I have a simple inductive type called 'constraint. Let's say in my context at some point I have:

a : constraint 

b : constraint

The goal is some proposition isFree involving b. so:

a : constraint

b : constraint

H: isFree (a).

------------------------------------

isFree(b)

What am I missing from proving this simple goal given H? I know if I had 'a=b' in the context, it would be simple but I don't.

And proof-irrelevance applies to Props only otherwise it would have given me a=b. 

In this case should I expect that isFree (a) implies isFree(b)?

--Bahman