I've implemented a proof system from a paper in Coq, as shown below. Term proof System
Require Import Ensembles.
Definition Var := nat.
Definition Name := nat.
Inductive Term: Type :=
| VarTerm (v: Var)
| PrivKeyTerm (k: Name)
| PubKeyTerm (k: Name)
| PairTerm (t1 t2: Term)
| PrivEncTerm (t: Term) (k: Name)
| PubEncTerm (t: Term) (k: Name).
Definition TermSet: Type := Ensemble Term.
Inductive dy : TermSet -> Term -> Prop:=
| ax {X: TermSet} {t: Term} (inH: In Term X t) : dy X t
| pk {X: TermSet} {k: Name} (kH: dy X (PrivKeyTerm k)) : dy X (PubKeyTerm k)
| splitL {X: TermSet} {t1 t2: Term} (splitH: dy X (PairTerm t1 t2)) : dy X t1
| splitR {X: TermSet} {t1 t2: Term} (splitH: dy X (PairTerm t1 t2)) : dy X t2
| pair {X: TermSet} {t1 t2: Term} (tH: dy X t1) (uH: dy X t2) : dy X (PairTerm t1 t2)
| sdec {X: TermSet} {t: Term} {k: Name} (encH: dy X (PrivEncTerm t k)) (kH: dy X (PrivKeyTerm k)): dy X t
| senc {X: TermSet} {t: Term} {k: Name} (tH: dy X t) (kH: dy X (PrivKeyTerm k)) : dy X (PrivEncTerm t k)
| adec {X: TermSet} {t: Term} {k: Name} (encH: dy X (PubEncTerm t k)) (keyH: dy X (PrivKeyTerm k)): dy X t
| aenc {X: TermSet} {t: Term} {k: Name} (tH: dy X t) (kH: dy X (PubKeyTerm k)) : dy X (PubEncTerm t k).
Now, I'm trying to prove a Normalisation property for this, as defined here. (Ignore the pub). Normalisation property
In trying to do this, I'm trying to implement a way of showing that a proof is normal. However, I am failing at this.
There are two ways I've been trying going about it. One is by building a relation on proofs called Normal, and trying to define constructors on the relation. I've been trying to build something of the sort
Inductive Normal {X: TermSet} {t: Term} : dy X t -> Prop := (* .. *),
However, I'm having trouble with this, particularly when I'm trying to implement any of the constructor rules, since Coq cant unify, say (PrivEncTerm t k) with the specific {t: Term} in the argument (used in dy X t).
The other approach I've been trying is defining a computation that calculates whether a proof is normal, however, I'm getting some weird type error when I do this.
Fixpoint isNormal {X: TermSet} {t: Term} (proof: dy X t) : bool :=
match proof with
| pair p1 p2 => andb (isNormal p1) (isNormal p2)
| senc pt pK => andb (isNormal pt) (isNormal pK)
| aenc pt pK => andb (isNormal pt) (isNormal pK)
| pk pK => isNormal pK
| ax _ => true
| splitL p => andb (isNormal p) (match p with | pair _ _ => false
| senc _ _ => false
| aenc _ _ => false
| pk _ => false
| splitL _ => true
| splitR _ => true
| sdec _ _ => true
| adec _ _ => true
| ax _ => true
end)
| splitR p => andb (isNormal p) (match p with | pair _ _ => false
| senc _ _ => false
| aenc _ _ => false
| pk _ => false
| _ => true
end)
| sdec pe pK => andb (isNormal pe) (andb (isNormal pK) (match pe with | pair _ _ => false
| senc _ _ => false
| aenc _ _ => false
| pk _ => false
| _ => true
end))
| adec pe pK => andb andb (isNormal pe) (andb (isNormal pK) (match pe with | pair _ _ => false
| senc _ _ => false
| aenc _ _ => false
| pk _ => false
| _ => true end))
end.
The "true of type bool" in question is in the last branch (the ax branch) of the match in the splitL case.
I have no idea how to resolve this, when I feel like the function itself is ok. Any advice on either of the two approaches would be really appreciated.
EDIT: I have understood the cause of the Weird Type Error, courtesy of @pierre-courtieu , however, fixing it by changing the definition of dy to return a Type isn't what I want. While in the meantime I'll be changing isNormal to return a Prop (which isnt working yet), any help on forming an inductive definition would be appreciated!
Your problem here (besides some superficial syntactic ones that the other answer already pointed out) is that you need to make a design decision: Do your derivations dy have "meaningful content" besides the question of whether they exist or not, and how meaningful is it?
If your proofs have meaningful content that you want to compute with; or if you want to define predicates about the "shape" of proofs, then you most likely want your proofs to be in Type. This means that Coq treats them as "data" and you can use it to write recursive functions on.
At first glance, this seems to be the case here. Unfortunately, this means that several things become more annoying. For example, Coq refuses to let you use them in "propositional" connectives like conjunction of disjunction. Instead, you need to use the corresponding connectives in Type, like pairs and sum types. You also need to have a good grasp of the elimination restriction (which is what prevents you from eliminating Props into Type) and its exceptions, in order to see ahead of time that your proof strategy can work. Also, your proof goals now all become exercises in dependently typed programming, which could potentially get very tricky.
An alternative that might work better here is to define (in Prop) a new judgment that corresponds to "normal form proofs," and then prove that both kinds of derivations are equivalent (which entails proving some sort of "normalization" procedure).
Which option is better is hard to say, that depends on what your future plans with this development are.
