CODEWITHSUNDEEP
coq
abhishek
abhishek

Reputation: 880

How can I write following inductive proposition in Coq without violating strict positivity?

S e := 
| def: (forall e', S e' -> S (App e e')) -> S e

I am trying to write logical relations based proof of strong normalization in Coq.

Upvotes: 2

Views: 121

Answers (1)

Tej Chajed
Tej Chajed

Reputation: 3948

You can write it as a Fixpoint over the structure of expressions:

Inductive expr :=
| Var (n:nat)
| Abs (n:nat) (e:expr)
| App (e1 e2: expr).

Fixpoint S (e:expr) : Prop :=
  match e with
  | Var n => True
  | Abs n e => True
  | App e1 e2 => S e2
  end.

Note that you can't say something like forall e', S e' -> subst e n e' in the Abs case because it doesn't recurse on a subterm. Instead, though, you can recurse on the structure of the type of e. I worked on something like this for Gödel's System T (lambda calculus with recursion over natural numbers): see https://github.com/tchajed/goedel-t/blob/master/SystemT.v#L538.

Upvotes: 1

Related Questions