Library CoqUniquenessTac
Provides a tactic for proving the uniqueness of objects.
From a list of types, compute the type of a curried function whose
arguments are those types.
Fixpoint arrow (xs : list Type) (res : Type) : Type :=
match xs with
| nil => res
| cons y ys => y -> arrow ys res
end.
From a list of types, compute the type of a heterogeneous list
whose elements are of those types. Heterogeneous lists are
represented as nested tuples.
Fixpoint tuple (xs : list Type) : Type :=
match xs with
| nil => unit
| cons y ys => (y * tuple ys)%type
end.
Apply a curried function to a heterogeneous list of arguments.
Definition apply_tuple
(xs : list Type) (res : Type) (f : arrow xs res) (arg : tuple xs)
: res.
Proof.
induction xs as [ | ? ? IH ]; simpl; intros res f arg.
exact f.
exact (IH res (f (fst arg)) (snd arg)).
Defined.
Reverse a list onto the given accumulator. Compared to
List.rev, this definition simplifies the implementation of
heterogeneous list reversal (see below).
Fixpoint tr_list_rev (A : Type) (xs : list A) (acc : list A) : list A :=
match xs with
| nil => acc
| cons y ys => tr_list_rev A ys (cons y acc)
end.
Implicit Arguments tr_list_rev [ A ].
Reverse a list.
Definition list_rev (A : Type) (xs : list A) : list A :=
tr_list_rev xs nil.
Implicit Arguments list_rev [ A ].
Reverse a heterogeneous list onto the given accumulator.
Definition tr_tuple_rev
(xs : list Type) (ab : tuple xs)
(acc : list Type) (acc' : tuple acc)
: tuple (tr_list_rev xs acc).
Proof.
induction xs as [ | ? ? IH ]; simpl; intros ab acc acc'.
exact acc'.
exact (IH (snd ab) (cons a acc) (fst ab, acc')).
Defined.
Reverse a heterogenous list.
Definition tuple_rev
(xs : list Type) (ab : tuple xs) : tuple (list_rev xs) :=
tr_tuple_rev xs ab nil tt.
This is the minimum set of facts about decidable equality that the
uniqueness tactic (defined below) requires.
Lemma eq_unit_dec : forall (x y : unit),
{x = y} + {x <> y}.
Lemma eq_pair_dec : forall (A B : Type),
(forall x y : A, {x = y} + {x <> y}) ->
(forall x y : B, {x = y} + {x <> y}) ->
(forall x y : A * B, {x = y} + {x <> y}).
Hint Resolve eq_unit_dec eq_pair_dec : eq_dec.
uniqueness analyzes goals of the form C x1 .. xn = q by
destructing q using the case tactic. It is mainly useful when
q is an object of an indexed inductive type Q, since it
generalizes the goal such that case will succeed. The argument
should be the number of indices to Q, and the indices should not
depend on each other.
Subgoals generated by the tactic will require one of three things: showing that the goal state is impossible, proving that equality at some type is decidable, and proving that any two objects of some type are equal. The tactic auto with eq_dec is used to discharge subgoals of the second form. The tactic auto is used to discharge subgoals of the third form.
Subgoals generated by the tactic will require one of three things: showing that the goal state is impossible, proving that equality at some type is decidable, and proving that any two objects of some type are equal. The tactic auto with eq_dec is used to discharge subgoals of the second form. The tactic auto is used to discharge subgoals of the third form.
Ltac uniqueness icount :=
intros;
try (match goal with |- _ = ?f _ => symmetry end);
let lhs := match goal with |- ?lhs = _ => constr:(lhs) end in
let rhs := match goal with |- _ = ?rhs => constr:(rhs) end in
let sort := match type of rhs with
| ?pred => match type of pred with ?sort => sort end
end
in
let rec get_pred_type i pred :=
match i with
| O => pred
| S ?n => match pred with ?f ?x => get_pred_type n f end
end
in
let pred := get_pred_type icount ltac:(type of rhs) in
let rec get_ind_types i pred acc :=
match i with
| O => acc
| S ?n => match pred with
| ?f ?x => let ind := type of x in
get_ind_types n f (@cons Type ind acc)
end
end
in
let ind_types := get_ind_types icount ltac:(type of rhs) (@nil Type) in
let rec get_inds i pred acc :=
match i with
| O => acc
| S ?n => match pred with ?f ?x => get_inds n f (x, acc) end
end
in
let inds := get_inds icount ltac:(type of rhs) tt in
let rind_types := constr:(list_rev ind_types) in
let rinds := constr:(tuple_rev ind_types inds) in
let core :=
constr:(fun (ainds : tuple rind_types)
(rhs : apply_tuple (list_rev rind_types)
sort
pred
(tuple_rev rind_types ainds))
=>
forall eqpf : rinds = ainds,
@eq (apply_tuple (list_rev rind_types)
sort
pred
(tuple_rev rind_types ainds))
(@eq_rect (tuple rind_types)
rinds
(fun rinds =>
apply_tuple (list_rev rind_types)
sort
pred
(tuple_rev rind_types rinds))
lhs
ainds
eqpf)
rhs)
in
let core := eval simpl in core in
let rec curry f :=
match type of f with
| forall _ : (unit), _ => constr:(f tt)
| forall _ : (_ * unit), _ => constr:(fun a => f (a, tt))
| forall _ : (_ * _), _ =>
let f' := constr:(fun b a => f (a, b)) in curry f'
end
in
let core := curry core in
let core := eval simpl in core in
let rec apply_core f args :=
match args with
| tt => constr:(f)
| (?x, ?xs) => apply_core (f x) xs
end
in
let core := apply_core core inds in
let core := constr:(core rhs) in
change lhs with (@eq_rect (tuple rind_types)
rinds
(fun rinds =>
apply_tuple (list_rev rind_types)
sort
pred
(tuple_rev rind_types rinds))
lhs
rinds
(refl_equal rinds));
generalize (refl_equal rinds);
change core;
case rhs;
unfold list_rev, tuple_rev in *;
simpl tr_list_rev in *;
simpl tr_tuple_rev in *;
repeat (match goal with
| |- (_, _) = (_, _) -> _ =>
let H := fresh in intros H; try discriminate; injection H
| _ => progress intro
end);
subst;
try (rewrite <- eq_rect_eq_dec; [ f_equal; auto | auto with eq_dec ]).
This page has been generated by coqdoc