Problem: this definition cannot be accepted by 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?
It can be encoded with a fixpoint:
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.
1 Like
Thank you for your beautiful solution. It is helpful for me.
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:
(* 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:
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)".
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.
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:
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.
1 Like
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:
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.