Being a Coq newbie, I am stuck on this problem. Hopefully, someone can help!
Given an encoding of finite types in Coq as below –
Fixpoint fin (n : nat) : Type :=
match n with
| 0 => False
| S m => option (fin m)
end.
Is it possible to define a function that lifts a value from fin (S n) to fin (S (S n)), while keeping the value the same. Thus, I am hoping to have the following equalities such as –
@up 2 (None : fin 2) = (None : fin 3)
@up 2 (Some None : fin 2) = (Some None : fin 3)
I thought of writing this –
Fixpoint up {n:nat} : fin (S n) -> fin (S (S n)) :=
fun p => match p with
| None => None
| Some p' => Some (up p)
But it is rejected. Intuitively I understand that it is possible because – members of fin 2 - None, Some None are members of fin 3 - None, Some None, Some (Some None) and so on. But I am not able to write the function for the same. I suspect its because the recursive definition has to deal with @up 0 where there should be an empty match, but I am not sure how to write this case. Any help would be appreciated! Thanks
You will need dependent pattern matching for your term to type-check properly.
Your structural parameter can only be n because this is the sole parameter of your Fixpoint. Your recursive call must be applied on a sub-term of n so you need a match on n somewhere.
I would favor the solution below, of return type fin n -> fin (S n), which is a bit more general, but you can specialize it to fin (S n) -> fin (S (S n)) later on of needed:
Fixpoint up {n} : fin n -> fin (S n) :=
match n return fin n -> fin (S n) with
| 0 => fun p => match p with end
| S n => fun p => match p with
| None => None
| Some q => Some (up q)
end
end.
Goal forall n, @up (S n) None = None.
Proof. reflexivity. Qed.
Goal forall n (p : fin n), @up (S n) (Some p) = Some (up p).
Proof. reflexivity. Qed.
Fixpoint fin2nat {n} : fin n -> nat :=
match n with
| 0 => fun p => match p with end
| S n => fun p => match p with
| None => 0
| Some p => S (fin2nat p)
end
end.
Eval compute in @fin2nat 8 (Some (Some (Some None))).
Eval compute in @fin2nat 20 (Some (Some (Some None))).
Fact up_correct {n} p : fin2nat (@up n p) = fin2nat p.
Proof.
induction n as [ | n IHn ] in p |- *; destruct p; simpl fin2nat; trivial.
f_equal; exact (IHn _).
Qed.
3
A useful way to debug is to go to replace your definition by its proof mode counterpart to see what is happening:
Fixpoint up {n:nat} : fin (S n) -> fin (S (S n)).
cbn in *. intro p; destruct p as [p' |].
- (* case Some *)
- (* case None *)
if you do, you’ll see that you are trying to build a term of type option (option (fin n)) knowing:
up: forall n : nat,
option (fin n) ->
option (option (fin n))
n: nat
p': fin n
--------------------------------
option (option (fin n))
so obviously up p does not type check
But actually you are thinking too much, here there is no need for induction as fin (S n) is option n so you can just define up {n} : fin n -> fin (S n) as Some:
Definition up {n:nat} : fin n -> fin (S n) := Some.
1