The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

On 4 août 2014, at 21:09, Jonathan 
<jonikelee AT gmail.com>
 wrote:

> On 08/04/2014 02:10 PM, Maxime Dénès wrote:
>> I meant phi returns Props, not booleans (although the same works with 
>> bool).
>> 
>> On 08/04/2014 02:08 PM, Maxime Dénès wrote:
>>> 
>>> The main concern is not extraction, but proof irrelevance. If you allow 
>>> unrestricted elimination from True \/ True, you can build the following 
>>> function:
>>> 
>>> Definition phi (p : True \/ True) : bool :=
>>>  match p with
>>>  | or_introl _ => True
>>>  | or_intror _ => False
>>>  end
>>> 
>>> Then you can refute proof irrelevance: assume it, deduce or_introl I = 
>>> or_intror I hence phi (or_introl I) = phi (or_intror I), hence True = 
>>> False, hence False.
> 
> Ah - that's the example I needed to jar me out of this rut!  Thanks, Maxime!
> 
> My naive view of rewrite rules as information preservation devices must be 
> untrue in some way.  But, what is the difference between those kinds of 
> bits in Prop can be created/destroyed arbitrarily by rewrite rules vs. 
> those that can't?
> 
> It is almost as though the bit in or is necessarily irrelevant (note: P \/ 
> Q <-> Q \/ P), independent of the proof irrelevance axiom, where the others 
> are contingently irrelevant based on inclusion or not of the proof 
> irrelevance axiom.  Or, "semi-contingently irrelevant" - with the proof 
> irrelevance axiom, they are, but without it they merely "might be".  But 
> that "might be" is strong enough to prevent arbitrary creation/destruction 
> due to rewrites.
> 
> Regardless, the case analysis rules have to prevent any and all irrelevant 
> bits from becoming relevant.

Hi,

You can already “eliminate" True \/ True in Type, assuming propositional 
proof-irrelevance,
but the eliminator chooses the branch.

Require Import ProofIrrelevance.

Definition true_true_elim 
  (P : True \/ True -> Type)
  (p : P (or_introl I))
  (x : True \/ True) : P x.
Proof.
  assert (or_introl I = x) by apply proof_irrelevance.
  rewrite <- H. apply p.
Defined.

Maybe another view could help, consider Prop as a universe built from 0, 1, x 
of Props and [A], where [A] “squashes”
the information in an arbitrary A : Type. 0, 1 and x have unrestricted 
eliminations to Type, whereas [A] is restricted 
to Prop contexts, and equality in all those type is irrelevant. Disjunction 
and existentials now become squashed, i.e, 
A \/ B := [A+B] and exists x : A. B := [{x : A & B}]. Now you can prove that 
1 and [1 + 1] are isomorphic using 
these rules, and hence eliminate hence on [1 + 1] in Type, but wouldn’t get 
to know which side is proven, the eliminator 
would be, again:

[1+1]-elim : (P : [1+1] -> Type) (p : forall x : 1, P (to-1+1 x)) (x : [1+1]) 
: P x.

Where (to-1+1 x : [1+1]) is irrelevant, whether you implement it using [left 
x] or [right x], [left 1] or [right 1],
these can’t be distinguished anymore. I think this reasoning is consistent 
with what Coq does,
see the Rooster and the Syntactic Bracket by A. Spiwack and H. Herbelin that 
describes this “decomposition”
of Prop in more details.

Hope this helps,
— Matthieu