The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 10/09/2012 05:25 AM, dan portin wrote:

  ρ₁ : nat
  ρ₂ : nat
  h : nat
  x₁ : nat
  h0 : nat
  x0 : nat
  t₁1 : T ρ₁ x0 h0
  t₁2 : T x0 x₁ h0
  t₁0 : T ρ₁ x₁ (succB true (S h))
  x1 : maxB E = S h
  x : Node E x0 t₁1 t₁2 ~= t₁0
  t₂ : T x₁ ρ₂ h
  ============================
   ∀ y : nat,
   mem y
     (projT2
        (joinL₁ N x₁ (existT (λ i : bool, T ρ₁ x₁ (succB i (S h))) true t₁0)
           t₂))
   ↔ mem y (projT2 (existT (λ i : bool, T ρ₁ x₁ (succB i (S h))) true t₁0))
     ∨ mem y t₂ ∨ x₁ = y

The second instance of existT _ true t₁0 simplifies as expected, but the first instance does not. I assume that the problem has to do with a conflict between the types that joinL₁ and the dependent pair expect. However, I cannot figure out how to rewrite using x1 and x in combination with generalizations of variables, pattern, and so forth, in order to generate a term which will simplify appropriately. The solution that I am working on is to write the proof term by hand, using elimination predicates in order to generate terms with the correct types. This doesn't seem like the best solution. Is there one?

You're closer than you think!  This is at all takes to get similar simplification to previous cases:
    simpl in *; subst; rewrite <- x; simpl.

What happens is that the [simpl in *] reduces [x1] so that it has only a variable on its lefthand side, at which point [subst] easily rewrites the goal so that all the tricky dependent type issues are gone.