The Coq mailing list

[Victor Porton <porton AT narod.ru>]

24.11.2011, 16:17, "Carlos Simpson" 
<Carlos.Simpson AT unice.fr>:
>  Dear Victor,
>  If you don't explain what you are planning to do with your arbitrary
>  proof, nobody will be able to help.
>  ---Carlos

I am attempting to prove (using the lemma [equal_foo]) the theorem [thm] 
stating that if data fields of two particular dependent record objects are 
equal then the records are equal.

See the code below.

[[[[
Parameter A : Set.
Parameter B : A -> Prop.

Structure Foo := mkFoo { a : A; b : B a }.

Definition tran {u v : Foo} (p : a u = a v) : B (a u) -> B (a v).
Proof.
  induction p.
  auto.
Defined.

(*Print tran.*)

Lemma equal_foo (u v : Foo) (p : a u = a v) : tran p (b u) = b v -> u = v.
Proof.
  intro H.
  destruct u as [x y].
  destruct v as [s t].
  simpl in * |- *.
  destruct p.
  simpl in H.
  rewrite H.
  reflexivity.
Qed.

Theorem thm (u v : Foo) : (a u = a v -> u = v).
proof.
  assume (a u = a v).
  let p be such that (p : a u = a v).
end proof. Qed.
]]]]

>  Selon Victor Porton 
> <porton AT narod.ru>:
>>   Dear David,
>>
>>   Thanks for your answer, but your answer is not a solution of my problem 
>> but a
>>   sly trick: instead of solving my problem you use an already stated fact
>>   P_true.
>>
>>   In order to get a proper solution I reformulate the problem in such a way
>>   that this trick becomes impossible (I hope).
>>
>>   [[[[
>>   Parameter P: Prop.
>>
>>   Theorem t: P -> True.
>>   proof.
>>     assume P.
>>     let X be such that (X : P).
>>   end proof. Qed.
>>   ]]]]
>>
>>   The "let" statement does not work with the error message:
>>
>>   Error: In environment
>>   _hyp : P
>>   X : P
>>   The term "X:P" has type "P" which should be Set, Prop or Type.
>>
>>   How to circumvent this problem? I need an arbitrary proof [X] of an 
>> assumed
>>   true proposition.
>>
>>   24.11.2011, 03:02, "David Pichardie" 
>> <david.pichardie AT inria.fr>:
>>>   Hi Victor,
>>>
>>>   Here the proof term of the statement "P" is "P_true" itself. Curry 
>>> Howard
>>   is behind the curtain.
>>>   If this is really your question then I think it is time to read the Coq 
>>> Art
>>   book.
>>>   Regards,
>>>
>>>   David.
>>>
>>>   Le 23 nov. 2011 à 13:56, Victor Porton a écrit :
>>>>    We should be able to take a proof of a true proposition. Is it
>>   implemented in Coq 8.3.pl2? My native attempt to do this steps on an 
>> error.
>>>>    [[[[
>>>>    Parameter P: Prop.
>>>>
>>>>    Axiom P_true: P.
>>>>
>>>>    Theorem t: True.
>>>>    proof.
>>>>     let X be such that (X : P).
>>>>    end proof. Qed.
>>>>    ]]]]
>>>>
>>>>    Error: In environment
>>>>    X : P
>>>>    The term "X:P" has type "P" which should be Set, Prop or Type.
>>>>
>>>>    I hope Coq allows to get around this, but I'm not sure.
>>>>
>>>>    --
>>>>    Victor Porton - http://portonvictor.org
>>   --
>>   Victor Porton - http://portonvictor.org
>  ------ ------ ------ ------ ------ ------ ------ ------ ------ ------ 
> ------
>
>  Carlos T. Simpson
>  C.N.R.S., Laboratoire J. A. Dieudonne, Universite de Nice-Sophia Antipolis
>
>  "Homotopy Theory of Higher Categories" now published!
>
>  Cambridge University Press, October 2011
>
>  http://www.cambridge.org/gb/knowledge/isbn/item6172978/
>
>  ------ ------ ------ ------ ------ ------ ------ ------ ------ ------ 
> ------
--
Victor Porton - http://portonvictor.org