[Agda] Q: Equational Reasoning

[Conor McBride]

Hi Hank

On 27 May 2009, at 19:56, Peter Hancock wrote:

> Conor McBride wrote:
>
>> I'd like to see a clearer Set/Prop distinction, with
>> support for the appropriate style in each. (Of course,
>> you need proof irrelevance to get away with it...)
>
> I've probably asked you (100s of times) before, but I've never got the
> hang of Props.  I'm particularly interested in
> Pi01 props, ie. (all x : N)...x..., where ...x...
> is decidable, and presumably a Prop.  Examples are
> the consistency of ZF, normalisation theorems,
> Goldbach's conjecture, FLT, or (so I'm told) Riemann's
> Hypothesis.  From a "behavioural" point of view,
> their proofs (should they exist) all look like \x.*

Depends who's looking. From the point of view of
a proof-checker, \x.* doesn't look like sufficient
evidence to me.

> .
>
> Are they Props?

In the sense that I'm talking about, yes. By Prop, I
often find I mean the universe

   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

So our friend

IsTrue : Bool -> Prop
IsTrue tt = TT
IsTrue ff = FF

means we get

All Nat \ n -> IsTrue (test n) : Prop

for any test : Nat -> Bool

>  In what sense are their proofs irrelevant?

I don't really like "irrelevant" as an adjective
describing proofs here: the phrase "proof
irrelevance" is not my choice. Operationally,
I guess I mean that the type system makes a
distinction between proofs and non-proofs, but
not between individual proofs. 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.

The elim forms for these Props are (if we set
things up appropriately)
    application for All, yielding a Prf
    projections for /\, yielding Prfs
    nothing for TT
    magic : Prf FF -> (X : Set) -> X

The only way proofs interfere with the computation
of values in sets is by magic, for which we must
prove FF. So proofs act like the "daimonos" of
Socrates, only to discourage, never to direct.

> I'm not being rhetorical, I just find something
> very paradoxical about Props, and would like to
> understand.

I know, and it is weird.

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".

Certainly, there's something outside of the
ordinary to understand here, and I'm not sure I
do yet.

Cheers

Conor