# An inductive definition failed with error "Non strictly positive occurrence..."

**URL:** <https://discourse.rocq-prover.org/t/an-inductive-definition-failed-with-error-non-strictly-positive-occurrence/2047>\
**Category:** Using Rocq\
**Created:** [September 19, 2023, 12:30pm UTC](https://discourse.rocq-prover.org/t/an-inductive-definition-failed-with-error-non-strictly-positive-occurrence/2047 "2023-09-19T12:30:20Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![zhengpushi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zhengpushi/32/773_2.png) [@zhengpushi](https://discourse.rocq-prover.org/u/zhengpushi)\
**Post date:** [September 19, 2023, 12:30pm UTC](https://discourse.rocq-prover.org/t/an-inductive-definition-failed-with-error-non-strictly-positive-occurrence/2047/1 "2023-09-19T12:30:20Z")

</div>

**Problem** : this definition cannot be accepted by Coq.

```coq
(* kind means different data types: value or array *)
Inductive kind :=
| kval
| karray (n:nat) (k:kind).

(* exp is expression with "kind" type, including: constant, negative, mapping *)
Inductive exp : kind -> Type :=
| e_cnst (n:nat) : exp kval
| e_neg (e:exp kval) : exp kval
(* An idea: mapping element of an array to result. But I failed. *)
| e_map (n:nat) (k:kind)
    (f:exp k -> exp k)
    (e:exp (karray n k)) : exp (karray n k).

(* Error: Non strictly positive occurrence of "exp" in *)
(* "forall (n : nat) (k : kind), (exp k -> exp k) -> exp (karray n k) -> exp (karray n k)". *)

```

**Question** :  
I know that the type of parementer `f` in `e_map` is the key wrong thing,  
because `exp k -> exp k` will cause a circular definition.  
But I argued that, `exp k` is a sub-type of `exp (karry n k)`,  
so it should not be a circular definition.

How can I let the Coq to know this relation, and accept my definition?  
Or, if the idea of encoding “mapping operation” in exp structure is wrong?

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [September 19, 2023, 1:50pm UTC](https://discourse.rocq-prover.org/t/an-inductive-definition-failed-with-error-non-strictly-positive-occurrence/2047/2 "2023-09-19T13:50:01Z")

</div>

It can be encoded with a fixpoint:

```coq
Inductive kind :=
| kval
| karray (n:nat) (k:kind).

Inductive exp_kval :=
| e_cnst (n:nat)
| e_neg (t:exp_kval)
.

Inductive exp_karray expk :=
| e_map (f : expk -> expk) (e:exp_karray expk).

Fixpoint exp k :=
  match k with
  | kval => exp_kval
  | karray n k => exp_karray (exp k)
  end.

(* we can define pseudo-constructors for exp *)

Definition e_cnst' (n:nat) : exp kval := e_cnst n.

Definition e_neg' (t : exp kval) : exp kval := e_neg t.

Definition e_map' (n:nat) (k:kind) (f:exp k -> exp k) (e:exp (karray n k)) : exp (karray n k)
  := e_map (exp k) f e.

(* and eliminator *)

Definition exp_rect
  (P:forall k, exp k -> Type)
  (v_cnst : forall n, P kval (e_cnst' n))
  (v_neg : forall t, P kval t -> P kval (e_neg' t))
  (v_map : forall n k (f:exp k -> exp k), (forall e, P _ (f e)) -> forall e:exp (karray n k), P _ e -> P _ (e_map' n k f e))
  : forall k e, P k e.
Proof.
  fix exp_rect 1.
  intros [|n k];simpl.
  - apply exp_kval_rect.
    + exact v_cnst.
    + exact v_neg.
  - apply exp_karray_rect.
    intros f e IHe.
    refine (v_map n k f _ e IHe).
    intros e';apply exp_rect.
Defined.
Print exp_rect.

```

---

<div class="post-metadata">

**Author:** ![zhengpushi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zhengpushi/32/773_2.png) [@zhengpushi](https://discourse.rocq-prover.org/u/zhengpushi)\
**Post date:** [September 19, 2023, 3:39pm UTC](https://discourse.rocq-prover.org/t/an-inductive-definition-failed-with-error-non-strictly-positive-occurrence/2047/3 "2023-09-19T15:39:05Z")

</div>

Thank you for your beautiful solution. It is helpful for me.

---

<div class="post-metadata">

**Author:** ![zhengpushi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zhengpushi/32/773_2.png) [@zhengpushi](https://discourse.rocq-prover.org/u/zhengpushi)\
**Post date:** [September 21, 2023, 1:14pm UTC](https://discourse.rocq-prover.org/t/an-inductive-definition-failed-with-error-non-strictly-positive-occurrence/2047/4 "2023-09-21T13:14:57Z")

</div>

Thank you for the method provided by @SkySkimmer. This method can  
indeed meet the requirements I originally proposed in this  
question. However, in fact, I raised a simplified question last time,  
and later I still ran into problems on the real problem. I was unable  
to establish an inductive-defined **exp** structure by simply changing the  
definition or designing multiple levels. I have been stuck for a few  
days, and I still want to ask for help from everyone. Here is my more  
realistic question.

My original intention was to: **establish an abstract syntax tree for**  
**the functional representation of vector expressions** , which can handle  
vectors of any dimension. With the operations of **map** and **reduce** ,  
vector addition, vector dot product, and matrix multiplication can be  
finally realized.

The specific code and error information are as follows:

```coq
  (* different types of data: scalar, any-dim-vector *)
  Inductive kind :=
  | knum
  | kary (n:nat) (k:kind)
  | kpair (k1 k2:kind).

  (* expressions to operate scalar or any-dim-vecotr *)
  Inductive exp : kind -> Type :=
  (* scalar operations *)
  | e_ScalarConst (n:nat) : exp knum
  | e_ScalarUnary (e:exp knum) : exp knum
  | e_ScalarBinary (e1 e2:exp knum) : exp knum
  (* vector operations *)
  | e_VectorMake (k:kind) (n:nat) (f:nat->exp k) : exp (kary n k)
  | e_VectorNth (k:kind) (n:nat) (e:exp (kary n k)) (i:nat) : exp k
  (* advanced operations: mapping, reduce. But, these operations failed! *)
  | e_VectorMap (k1 k2:kind) (n:nat) (e:exp (kary n k1)) 
    (f:exp k1->exp k2) : exp (kary n k2)
  | e_VectorReduce (k1 k2:kind) (n:nat) (e:exp (kary n k1)) 
    (g:exp k1->exp k2->exp k2) (e0:exp k2) : exp k2.

```

The problems are: the parameter `f:exp k1->exp k2` or `g:exp k1->exp k2->exp k2`  
are disallowed in Coq. Error message are:

```auto
  Error: Non strictly positive occurrence of "exp" in
  "forall (k1 k2 : kind) (n : nat), exp (kary n k1) -> (exp k1 -> exp k2) -> 
  exp (kary n k2)".

```

---

<div class="post-metadata">

**Author:** ![zhengpushi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zhengpushi/32/773_2.png) [@zhengpushi](https://discourse.rocq-prover.org/u/zhengpushi)\
**Post date:** [September 21, 2023, 1:38pm UTC](https://discourse.rocq-prover.org/t/an-inductive-definition-failed-with-error-non-strictly-positive-occurrence/2047/5 "2023-09-21T13:38:03Z")

</div>

The reason why I want to define all vector operations in an inductive definition is because I think that all operations on vectors can be realized through these primitive operations, and I can perform program transformation and optimization on AST. If there can be an inductive definition, the operation on vectors becomes a tree structure, which will be easy to manipulate. If some way could be found to represent all abstract representations of vector expressions, I’d be happy to accept that as well.

In addition, when using the `Unset Positivity Checking` option, Coq will also accept these definitions, but will not generate induction principles and recursors.

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [September 21, 2023, 2:31pm UTC](https://discourse.rocq-prover.org/t/an-inductive-definition-failed-with-error-non-strictly-positive-occurrence/2047/6 "2023-09-21T14:31:53Z")

</div>

In the original question you said

> But I argued that, exp k is a sub-type of exp (karry n k),  
> so it should not be a circular definition.

This is indeed why the fixpoint I wrote works, and it’s not true for map (`exp k1` is not smaller than `exp (kary n k2)`) and reduce (`exp k1` `exp k2` vs `exp k2`).

and if you unset positivity checking you get non terminating fixpoints:

```auto

Inductive kind :=
| knum
| kary (n:nat) (k:kind)
.

Unset Positivity Checking.

Inductive exp : kind -> Type :=
| e_ScalarConst (n:nat) : exp knum
| e_VectorMake (k:kind) (n:nat) (f:nat->exp k) : exp (kary n k)
| e_VectorReduce (k1 k2:kind) (n:nat) (e:exp (kary n k1))
    (g:exp k1->exp k2->exp k2) (e0:exp k2) : exp k2.

Set Positivity Checking.

Fixpoint dummy {k} : exp k :=
  match k with
  | knum => e_ScalarConst 0
  | kary n k => e_VectorMake _ _ (fun _ => dummy)
  end.

Definition t := exp knum.

Definition lam (f:t -> t) : t := e_VectorReduce knum _ 0 dummy (fun _ => f) dummy.

Definition app (x:t) (y:t) : t := e_VectorReduce knum _ 0 dummy (fun _ _ => x) y.

Fixpoint eval k (e:exp k) {struct e} : nat.
Proof.
  (* if e looks like (app (lam f) x) do "eval (f x)", otherwise return 0 *)
  destruct e;[exact 0|exact 0|].
  destruct (g dummy dummy);[exact 0|exact 0|].
  destruct k0,k2.
  exact (eval _ (g0 dummy e2)).
  all:exact 0.
Defined.

Definition delta : t := lam (fun x => app x x).
Definition omega : t := app delta delta.

Definition bad := eval _ omega.

Eval lazy in bad. (* loops *)

```

> The reason why I want to define all vector operations in an inductive definition is because I think that all operations on vectors can be realized through these primitive operations

I’m not sure having subexpressions of type `exp _ -> exp _` makes sense for this goal.

---

<div class="post-metadata">

**Author:** ![zhengpushi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zhengpushi/32/773_2.png) [@zhengpushi](https://discourse.rocq-prover.org/u/zhengpushi)\
**Post date:** [September 22, 2023, 3:46am UTC](https://discourse.rocq-prover.org/t/an-inductive-definition-failed-with-error-non-strictly-positive-occurrence/2047/7 "2023-09-22T03:46:57Z")

</div>

Thank you @SkySkimmer for your generosity in giving so much technical guidance.  
I’m currently trying to use a two-layer structure to achieve my needs. as follows:

```coq
Inductive kind :=
| knum
| kary (n:nat) (k:kind)
.
Definition kmat r c k := kary r (kary c k).

Inductive exp : kind -> Type :=
| e_Var (k:kind) (x:nat) : exp k
| e_ScalarConst (n:nat) : exp knum
| e_ScalarNeg (e:exp knum) : exp knum
| e_VectorMake (k:kind) (n:nat) (f:nat->exp k) : exp (kary n k)
| e_VectorIdx (k:kind) (n:nat) (e:exp (kary n k)) : exp k
| e_VectorMakeIdx (k:kind) (n:nat) (e:exp k) : exp (kary n k)
| e_VectorNth (k:kind) (n:nat) (e:exp (kary n k)) (i:nat) : exp k.

(* high level expressions *)
Inductive expHL : kind -> Type :=
| e_exp (k:kind) (e:exp k) : expHL k
| e_VectorMap (k1 k2:kind) (n:nat) (e:exp (kary n k1))
    (f:exp k1->exp k2) : expHL (kary n k2)
| e_VectorReduce (k1 k2:kind) (n:nat) (e:exp (kary n k1))
    (g:exp k1->exp k2->exp k2) (e0:exp k2) : expHL k2.

(* Fold a sequence *)
Fixpoint fold_f {A B} (seq:nat->A) (n:nat) (f:A->B->B) (b:B) : B :=
  match n with
  | O => b
  | S n' => fold_f seq n' f (f (seq n') b)
  end.

(* Convert from expHL to exp *)
Definition expHL_to_exp {k:kind} (eh: expHL k) : exp k.
  destruct eh.
  - apply e.
  - apply (e_VectorMakeIdx k2 n (f (e_VectorIdx k1 n e))).
  - apply (fold_f (e_VectorNth k1 n e) n g e0).
Defined.

Coercion expHL_to_exp : expHL >-> exp.

(* Operations for vector and matrix *)
Example vneg {n} (e:exp (kary n knum)) : exp (kary n knum) :=
  e_VectorMap _ _ _ e e_ScalarNeg.

Example mneg {r c} (e:exp (kmat r c knum)) : exp (kmat r c knum) :=
  e_VectorMap _ _ _ e vneg. (* Now, we can use `map` freely. *)

```

I tried as best I could to keep going. If I can’t proceed, I’ll bring it up and discuss it again.