2
$\begingroup$

In the code below:

Require Import Bool.

Fixpoint F (n: nat): Set := match n with
    | 0 => bool
    | S n' => bool -> (F n')
end.

Fixpoint B (n: nat): Set := match n with
    | 0 => bool
    | 1 => bool
    | S n' => bool * (B n')
end.

Fixpoint apply_f {n: nat} (f: (F n)) (x: (B n)) := match n with
    | 0 => f
    | 1 => f x
    | S n' => apply_f (f (fst x)) (snd x)
end.

I am attempting to define an n-ary boolean function type (F n) and a boolean n-tuple (B n). All is fine and well until I attempt to define a function to apply some f: (F n) to an n-tuple (B n). For n=0 it's simply the case that f is the constant function, thus all is well. For n=1 however the following error occurs:

Illegal application (Non-functional construction): 
The expression "f" of type "F n" cannot be applied to the term
 "x" : "B n"

So, I simply changed the line from | 1 => f x to | 1 => f (x: bool), attempting to typecast x: (B 1) to bool. However, the following error occurs.

In environment
apply_f : forall n : nat, F n -> B n -> F n
n : nat
f : F n
x : B n
n0 : nat
n1 := 0 : nat
The term "x" has type "B n" while it is expected to have type "bool".

I have tried various other solutions, but none of it seems to work, given my lack of experience with logic and functional programming overall. Thus, I am now resorting to asking this very question here on Proof Stack Exchange: How do I specify, in the n=1 case, to Coq, that x: (B 1) is equivalent to x: bool?

$\endgroup$
1
  • $\begingroup$ Firstly, thank you for telling me what I'm looking for, I'm sure the search term will be helpful. Secondly, seems like your solution just delays the problem further, as I will either have to write infinitely many lines of code (which would interrupt my precious tea time forevermore), or if I try an alternate solution: Fixpoint apply_f {n : nat} : F n -> B n -> bool := match n return F n -> B n -> bool with | 0 => fun f x => f | S n' => fun f x => apply_f (f (fst x)) (snd x) end. the exact same problem of Coq not realizing nat * nat = B 2 occurs. $\endgroup$
    – E030E03
    Aug 19, 2023 at 11:57

2 Answers 2

1
$\begingroup$

Sometimes, it's easier to do programming with dependent types in Ltac rather than Gallina. Below, I've more or less transliterated your program so that the matching is done in Ltac (though I also use induction rather than Fixpoint, as is idiomatic). The tactics are generally set up so that anything matched on (n) is partially instantiated appropriately (to O and S n) everywhere in the goal and context.

Require Import Bool.

Fixpoint F (n: nat): Set := match n with
    | 0 => bool
    | S n' => bool -> (F n')
end.

Fixpoint B (n: nat): Set := match n with
    | 0 => bool
    | 1 => bool
    | S n' => bool * (B n')
end.

Definition apply_f {n: nat} (f: (F n)) (x: (B n)): bool.
Proof.
  induction n as [|n IH].
  - exact f.
  - destruct n as [|n].
    * exact (f x).
    * exact (IH (f (fst x)) (snd x)).
Defined.

Incidentally, I think you get a cleaner program if you remove the special case for 0 in B, as in:

Fixpoint F (n: nat): Set := match n with
    | 0 => bool
    | S n' => bool -> (F n')
end.

Fixpoint B (n: nat): Set := match n with
    | 0 => unit
    | S n' => bool * (B n')
end.

Definition apply_f {n: nat} (f: (F n)) (x: (B n)): bool.
Proof.
  induction n as [|n IH].
  - exact f.
  - exact (IH (f (fst x)) (snd x)).
Defined.
```
$\endgroup$
3
  • $\begingroup$ Thank you very much for the solution! Though, I now have a few more questions followup: 1. What does it mean to define something in Ltac? Why are we proving a definition? Is it proving that the definition does indeed return that type??? I am very confused. 2. This, while is a solution, doesn't seem to address the issue in my program and my knowledge: I still know not how to typecast nor enforce types. This shows in the fact that I have to write ` Compute apply_f (andb: F 2) (true, false). ` instead of only writing ` Compute apply_f andb (true, false). `. $\endgroup$
    – E030E03
    Aug 19, 2023 at 18:28
  • $\begingroup$ Ltac is the tactic language. Tactics are commands that refine a partial term, eventually hopefully resulting in a full term. Tactics apply just as well to program terms as proof terms, using the fact that proofs are a special case of programs in MLTT/CIC. Often people don't like using Ltac to produce programs because it can obscure the computational behaviour of the program (which tends to matter less for proofs). For example, in the first apply_f, it's not as easy to see which values each case deals with as if we'd used a match with named patterns. $\endgroup$
    – James Wood
    Aug 20, 2023 at 12:42
  • $\begingroup$ It's a bit weird that Ltac sections are introduced by Proof., but I guess that's for historical reasons and the fact that the usual use of Ltac is in producing proofs. Using Defined. at the end, rather than Qed., is significant, and means that the computational behaviour is retained – i.e, the function actually runs. $\endgroup$
    – James Wood
    Aug 20, 2023 at 12:46
0
$\begingroup$

Just a remark about n being implicit:

Let's consider James's modification.

Fixpoint apply_f {n: nat} : F n -> B n -> bool :=
  match n with 
  | 0 => fun f x => f
  | S _ => fun f x => apply_f (f (fst x)) (snd x)
  end.

In the next query, Coq doesn't infer n from the other arguments.

Require Import Bool.
Fail Compute apply_f orb (true, (false, tt)).

There are many ways to make n explicit.

Compute apply_f (orb: F 2) (true, (false, tt)).

Compute let orb := orb: F 2 in
   apply_f orb (true, (false, tt)).

Compute apply_f (n:=2) andb (true, (false, tt)).

Arguments apply_f : clear implicits. 

Compute apply_f 2 orb (true, (false, tt)).
$\endgroup$
2
  • $\begingroup$ Hm, is there perhaps a way to ensure F 2 is always equated with bool -> bool -> bool? I kinda wish for Coq to automatically infer the arity of my function. $\endgroup$
    – E030E03
    Aug 19, 2023 at 18:35
  • $\begingroup$ @E030E03 See dl.acm.org/doi/10.1145/3331554.3342604 for an explanation of exactly what you need to infer the number from the type. IIRC, the development of this paper included strengthening of Agda's unification abilities. The one I remember is inference of definitional injectivity of definitions. $\endgroup$
    – James Wood
    Aug 20, 2023 at 12:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.