The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Okay, here it goes (proof script).

Require Import Utf8.

Set Implicit Arguments.

Inductive ilist A: nat -> Type :=
 | Nil: ilist A 0
 | Cons: forall n, A -> ilist A n -> ilist A (S n).

Fixpoint imap A B n (f: A -> B) (L: ilist A n): ilist B n.
Proof.
 induction L. exact (Nil _). exact (Cons (f a) IHL).
Defined.

Fixpoint In A n x (L: ilist A n) :=
 match L with
 | Nil _ => True
 | Cons a l => x = a \/ In x l
 end.

Fixpoint Fun (A B: Type) n :=
 match n with
 | O => B
 | S m => A → Fun A B m
 end.

Definition Fun_application A B n (f: Fun A B n) (L: ilist A n): B.
Proof.
    induction L.
        exact f.
        exact (IHL (f a)).
Defined.

Print Fun_application.

Definition function A n := Fun A A n.
Definition relation A n := Fun A bool n.

Definition function_application A n (f: function A n) (x: ilist A n) :=
    Fun_application A f x.
Definition relation_application A n (f: relation A n) (x: ilist A n) :=
    Fun_application bool f x.

Structure Language A B := {
   function_arity: A → nat;
   relation_arity: B → nat
}.

Structure Structure A B (L: Language A B) domain := {
    function_interpretation: ∀ x, function domain (function_arity L x);
    relation_interpretation: ∀ x, relation domain (relation_arity L x)
}.

Definition Assignment A := nat -> A.

Inductive Term A B (L: Language A B) :=
 | variable: nat -> Term L
 | function_node: forall x, parameters L (function_arity L x) -> Term L
with parameters A B (L: Language A B): nat -> Type :=
 | p0: parameters L O
 | pS: forall n, Term L -> parameters L n -> parameters L (S n).

Require Program.

Program Fixpoint interpretation A B domain (L: Language A B) (s: Structure L domain) (x: Assignment domain) (t: Term L) : domain :=
 match t with
 | variable _ x0 => x x0
 | function_node x0 l => term_fun s x (function_interpretation s x0) l
 end
with term_fun A B domain (L: Language A B) (s: Structure L domain) (x: Assignment domain) n (F: function domain n)  (P: parameters L n): domain :=
 match n with
 | O => _
 | S m => match P with
          | p0 _ => _
          | pS x0 l0 => term_fun s x (_ (interpretation s x x0)) l0
          end
 end.
Obligations.
Next Obligation.
 exact F. Defined.
Obligations.
Next Obligation.
 exact (F x1). Defined.
Obligations.
Next Obligation.

 

The last line 'Next Obligation' results in such error message:
<< Anomaly: Could not find a solvable obligation.. Please report. >>

(I'm using Coq 8.5p2 beta)

What to do with this?

What I want from this function, I will write later (probably it's necessary), because I'm in hurry.

In short - It's language term evaluation, if meanings of Language terms are given (by Structure) and variable assignments are given too (by Assignment).

 

P.S. Is there some good tutorial for defining such functions?