The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Monday, April 30, 2012 01:31:51 AM AUGER Cédric wrote:
> I think you cannot naïvely remove [l] and [r] from binary_search_tree
> without having bad surprises.

*Of course* you would need to be careful when writing your functions that you 
don't use the removed constructor arguments, and granted, in complex cases 
that might be more trouble than it's worth.  To take a silly example:

Fixpoint find_bounds {l r} (t:binary_search_tree l r) (x:A) :
  option (option A * option A) :=
match t with
| empty_bst _ _ => None
| bst_node _ _ y left_subtree right_subtree _ =>
  match lt_eq_gt x y with
  | IsLt _ => find_bounds left_subtree x
  | IsEq _ => Some (l, r)
  | IsGt _ => find_bounds right_subtree x
  end
end.

This one wouldn't extract with those eliminated constructor arguments.  But 
this variant would:

Definition array_appl {A:Type} {P:A->Type} (f:forall x:A, P x) (x:A) : P x :=
  f x.

Notation "[ x ; y ; .. ; z ] @> f" :=
  (array_appl .. (array_appl (array_appl f x) y) .. z)
  (left associativity, at level 91).

Fixpoint find_bounds' {l r} (t:binary_search_tree l r) (x:A) {struct t} :
  option (option A * option A) :=
[ eq_refl l ; eq_refl r ] @>
match t in (binary_search_tree l' r') return
  (l' = l -> r' = r -> option (option A * option A)) with
| empty_bst _ _ => fun _ _ => None
| bst_node _ _ y left_subtree right_subtree _ =>
  match lt_eq_gt x y with
  | IsLt _ => fun left_eq _ =>
    find_bounds'
      (match left_eq in (_ = l'') return (binary_search_tree l'' _) with
       | eq_refl => left_subtree
       end)
      x
  | IsEq _ => fun _ _ => Some (l, r)
  | IsGt _ => fun _ right_eq =>
    find_bounds'
      (match right_eq in (_ = r'') return (binary_search_tree _ r'') with
       | eq_refl => right_subtree
       end)
      x
  end
end.

(BTW, I couldn't find a way to eliminate the equalities here.  My first 
instinct 
was to try convoying versions of find_bounds' with l, respectively r fixed; 
but 
it seems the guardedness checker isn't smart enough to be able to handle 
that.)
-- 
Daniel Schepler