[Agda] Q: Equational Reasoning

[Andreas Abel]

Hi Conor,

On May 27, 2009, at 10:24 PM, Conor McBride wrote:
>  data Prop : Set1 where
>    All : (S : Set) -> (S -> Prop) -> Prop
>    _/\_ : Prop -> Prop -> Prop
>    TT : Prop
>    FF : Prop
>
>  Prf : Prop -> Set
>  Prf (All S P) = (s : S) -> Prf (P s)
>  Prf (P /\ Q)  = Sigma (Prf P) \ _ -> Prf Q
>  Prf TT        = One
>  Prf FF        = Zero

>  Any two inhabitants
> of Prf P are definitionally equal, but that does
> *not* mean that * : Prf P if any p : Prf P,
> even if P is closed.

What is so bad about this rule?

   Gamma |- p : Prf P
   -------------------------
   Gamma |- * : Prf P

Of course, it destroys type checking, thus, "*" should not be allowed  
in the input syntax of you proof checker.
But otherwise, adding this rule does not change the theory, at least  
that is what we believe to have proven in  Abel, Coquand, Miquel,  
TLCA'09.  Meaning, if you have a derivation of

   Gamma |- t : T

and * does not appear in Gamma, t, T, then you get one without this  
rule.

> One way to expose the weirdness is to consider
> checking judgmental equality by comparing
> normal forms syntactically, for some (perhaps
> type-directed) notion of normalization. One might
> take normal forms to indicate the "meaning"
> of terms, but I'm not a philosopher and feel
> embarrassed about meaning. One might then hope
> that judgmental equality would exactly capture
> "meaning the same" in this sense.
>
> But if you ask me in this sense, "what is the
> meaning of a proof?" then I'm in trouble: I
> can't replace all proofs with a dummy (e.g., *)
> because I can't recheck the dummy, but then I'm
> stuck distinguishing proofs if they have
> syntactically distinct normal forms. "Proof
> irrelevance", in the sense that I want, is
> outside this picture.
>
> What I need, if I'm to fix this problem is some
> way to weaken the syntactic identity of normal
> forms. If you extend the syntax of normal forms
> with some way to mark parts of terms as proofs
> without deleting them -- putting them in a box
> perhaps. Maybe we identify normal forms
> syntactically only up to what's outside boxes.
> Then we might be get some sort of recheckable
> normal form which could act as a "meaning",
> with all proofs of the same proposition "meaning
> the same".

However, if you do not need to type check your normal forms, but only  
compute them to check equality, it seems safe to collapse all boxes to  
*.

Cheers,
Andreas