The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Hi all,

Le 21 août 08 à 12:02, Conor McBride a écrit :

> The Agda typechecker is doing all Samuel's equational reasoning
> (effectively first-order unification by hand) externally to the
> type theory and just accepting that this function is ok. Of course,
> it's possible to automate the equational reasoning inside the type
> theory: aren't there new dependent induction/inversion tactics
> which do that in Coq? Perhaps they might tidy up Samuel's proof.
> If anyone can point me to a beta of Coq 8.2 for a G4 mac, I'll
> happily try it out.

Yes you can, but Coq needs JMeq_eq to be convinced, so this won't
compute:

<<
(*=
======================================================================*)

Require Import Bvector.

Implicit Arguments Vcons [A n].

(*=
======================================================================*)

Inductive Bounded : nat -> Set :=
|   Zero : forall (n : nat), Bounded (S n)
|   Succ : forall (n : nat), Bounded n -> Bounded (S n)
.

Implicit Arguments Succ [n].

(*=
======================================================================*)

Fixpoint Bounded_to_nat (n : nat) (i : Bounded n) {struct i} : nat :=
match i with
|   Zero _     => 0
|   Succ n0 i0 => S (Bounded_to_nat n0 i0)
end
.

Implicit Arguments Bounded_to_nat [n].

Require Import Equality.

(*=
======================================================================*)

Definition prefix : forall (m : nat) (i : Bounded (S m)) (a : Type),
vector a m -> vector a (Bounded_to_nat i).
intro.
induction m as [| n].
(* Case m = 0 *)
intros i ; dependent destruction i.
apply (Vnil a).
inversion i.
(* Case m = S n *)
intros i ; dependent destruction i.
(* Case i = Zero *)
apply (Vnil a).
(* Case i = Succ j *)
simpl.
dependent destruction X.
apply (Vcons a0 (IHn i a X)).
Defined.

Implicit Arguments prefix [m a].

(*=
======================================================================*)

Definition test_vec := Vcons 10 (Vcons 20 (Vcons 30 (Vnil nat))).

Eval compute in prefix (Zero 3) test_vec.

Eval compute in prefix (Succ (Zero 2)) test_vec.

Eval compute in prefix (Succ (Succ (Zero 1))) test_vec.

Eval compute in prefix (Succ (Succ (Succ (Zero 0)))) test_vec.

(*=
======================================================================*)
>>

One can also use Program to define it. The generated obligations make  
use of
JMeq_eq again, and the last one is particularly complicated and  
requires the
additional manual destruction of an index to simplify the equations.

<<
Require Import Program.

Program Fixpoint prefix' {a m} (v : vector a m) : Π (i : Bounded (S  
m)), vector a (Bounded_to_nat i) :=
match v with
| Vnil => λ i, Vnil a
| Vcons x n' v' => λ i,
match i with
 | Zero _ => Vnil a
 | Succ n'' i' => Vcons x (prefix' v' i')
end
end.

Next Obligation.
dependent destruction i. simpl. reflexivity.
inversion i.
Defined.

Next Obligation.
dependent destruction i. simpl. reflexivity.
Defined.

Next Obligation.
simplify_eqs. destruct n'' ; simpl_depind. subst.
simplify_eqs. reflexivity.
Qed.
>>

--
Matthieu Sozeau