comparison src/Equality.v @ 488:31258618ef73

Incorporate feedback from Nathan Collins
comparison
equal inserted replaced
487:8bfb27cf0121 488:31258618ef73
626 match pf in (_ = ls) return (fhlist B ls) with 626 match pf in (_ = ls) return (fhlist B ls) with
627 | eq_refl => (a0, f) 627 | eq_refl => (a0, f)
628 end 628 end
629 ]] 629 ]]
630 630
631 The conclusion has gotten markedly simpler. It seems counterintuitive that we can have an easier time of proving a more general theorem, but that is exactly the case here and for many other proofs that use dependent types heavily. Speaking informally, the reason why this kind of activity helps is that [match] annotations only support variables in certain positions. By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood. 631 The conclusion has gotten markedly simpler. It seems counterintuitive that we can have an easier time of proving a more general theorem, but that is exactly the case here and for many other proofs that use dependent types heavily. Speaking informally, the reason why this kind of activity helps is that [match] annotations contain some positions where only variables are allowed. By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood.
632 632
633 In this case, it is helpful to generalize over our two proofs as well. *) 633 In this case, it is helpful to generalize over our two proofs as well. *)
634 634
635 generalize pf pf'. 635 generalize pf pf'.
636 (** [[ 636 (** [[