matita/matita/lib/hott/Overture.ma

   1 include "types.ma".
   2
   3 (* * * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *)
   4
   5 definition relation ≝ λA : Type[0]. A → A → Type[0].
   6
   7 record Reflexive (A) (R : relation A) : Type[0] ≝ {
   8   reflexivity : ∀x : A. R x x
   9 }.
  10
  11 record Symmetric (A) (R : relation A) : Type[0] ≝ {
  12   symmetry : ∀x,y. R x y → R y x
  13 }.
  14
  15 record Transitive (A) (R : relation A) : Type[0] ≝ {
  16   transitivity : ∀x,y,z. R x y → R y z → R x z
  17 }.
  18
  19 (*Tactic Notation "etransitivity" open_constr(y) :=
  20   let R := match goal with |- ?R ?x ?z => constr:(R) end in
  21   let x := match goal with |- ?R ?x ?z => constr:(x) end in
  22   let z := match goal with |- ?R ?x ?z => constr:(z) end in
  23   refine (@transitivity _ R _ x y z _ _).*)
  24
  25 (*Tactic Notation "etransitivity" := etransitivity _.*)
  26
  27 (* * We would like to redefine [symmetry], which is too smart for its own good, as follows:
  28
  29 <<
  30 Ltac symmetry := refine (@symmetry _ _ _ _ _ _).
  31 >>
  32
  33 But this gives "Error: in Tacinterp.add_tacdef: Reserved Ltac name symmetry.".  This might be fixed with https://coq.inria.fr/bugs/show_bug.cgi?id=3113.  For now, you can [apply symmetry] or [eapply symmetry].  (Note that we can get around this error message by using [Tactic Notation "symmetry"], but, confusingly, this tactic notation never gets called. *)
  34
  35 (* * ** Basic definitions *)
  36
  37 (*CSC: was a Notation in Coq *)
  38 definition idmap : ∀A:Type[0]. A → A ≝ λA,x.x.
  39
  40 (* * Composition of functions. *)
  41 definition compose ≝ λA,B,C: Type[0]. λg : B → C. λf : A → B.
  42  λx. g (f x).
  43
  44 interpretation "compose" 'compose g f = (compose ??? g f).
  45
  46 (* * ** The groupoid structure of identity types. *)
  47
  48 (* * The results in this file are used everywhere else, so we need to be extra
  49     careful about how we define and prove things.  We prefer hand-written terms,
  50     or at least tactics that allow us to retain clear control over the
  51     proof-term produced. *)
  52
  53 (* * We define our own identity type, rather than using the one in the Coq
  54      standard library, so as to have more control over transitivity, symmetry
  55      and inverse.  It seems impossible to change these for the standard
  56      eq/identity type (or its Type-valued version) because it breaks various
  57      other standard things.  Merely changing notations also doesn't seem to
  58      quite work. *)
  59 inductive paths (A : Type[0]) (a : A) : A → Type[0] ≝
  60   idpath : paths A a a.
  61
  62 interpretation "paths" 'eq t a b = (paths t a b).
  63
  64 (*CSC: MANCANO GLI HINT *)
  65 definition reflexive_paths: ∀A:Type[0]. Reflexive … (paths A) ≝
  66  λA. mk_Reflexive … (idpath A).
  67
  68 (* * We define equality concatenation by destructing on both its arguments, so
  69   that it only computes when both arguments are [idpath]. This makes proofs
  70   more robust and symmetrical. Compare with the definition of [identity_trans]. *)
  71
  72 definition concat : ∀A : Type[0]. ∀x,y,z: A. x = y → y = z → x = z.
  73  #A #x #y #z #p #q cases q cases p %
  74 qed.
  75
  76 (*CSC: MANCANO GLI HINT *)
  77 definition transitive_paths: ∀A:Type[0]. Transitive … (paths A) ≝
  78  λA.mk_Transitive … (concat A).
  79
  80 (* * The inverse of a path. *)
  81 definition inverse : ∀A : Type[0]. ∀x,y : A. x = y → y = x.
  82  #A #x #y * %
  83 qed.
  84
  85 (*CSC: MANCANO GLI HINT *)
  86 definition symmetric_paths: ∀A:Type[0]. Symmetric … (paths A) ≝
  87  λA. mk_Symmetric … (inverse A).
  88
  89 (* * Note that you can use the built-in Coq tactics [reflexivity] and [transitivity]
  90     when working with paths, but not [symmetry], because it is too smart for its
  91     own good.  Instead, you can write [apply symmetry] or [eapply symmetry]. *)
  92
  93 (* * The identity path. *)
  94 interpretation "idpath" 'idpath = (idpath ??).
  95
  96 interpretation "concat" 'append g f = (concat ???? g f).
  97
  98 interpretation "inverse" 'invert p = (inverse ??? p).
  99
 100 (* * An important instance of [paths_rect] is that given any dependent type, one
 101   can _transport_ elements of instances of the type along equalities in the base.
 102
 103    [transport P p u] transports [u : P x] to [P y] along [p : x = y]. *)
 104 definition transport: ∀A : Type[0]. ∀P: A → Type[0]. ∀x,y : A. x=y → P x → P y.
 105  #A #P #x #y * //
 106 qed.
 107
 108 (* * Transport is very common so it is worth introducing a parsing notation for it.
 109   However, we do not use the notation for output because it hides the fibration,
 110   and so makes it very hard to read involved transport expression.*)
 111
 112 interpretation "transport" 'transport F p x = (transport ? F ?? p x).
 113
 114 (* * Having defined transport, we can use it to talk about what a homotopy
 115   theorist might see as "paths in a fibration over paths in the base"; and what
 116   a type theorist might see as "heterogeneous eqality in a dependent type".
 117
 118   We will first see this appearing in the type of [apD]. *)
 119
 120 (* * Functions act on paths: if [f : A -> B] and [p : x = y] is a path in [A],
 121      then [ap f p : f x = f y].
 122
 123    We typically pronounce [ap] as a single syllable, short for "application"; but it may also be considered as an acronym, "action on paths". *)
 124
 125 definition ap: ∀A,B: Type[0]. ∀f:A → B. ∀x,y: A. x = y → f x = f y.
 126  #A #B #f #x #y * %
 127 qed.
 128
 129 (* * We introduce the convention that [apKN] denotes the application of a K-path
 130    between functions to an N-path between elements, where a 0-path is simply a
 131    function or an element. Thus, [ap] is a shorthand for [ap01]. *)
 132 (*CSC: WAS A NOTATION *)
 133 definition ap01 := ap.
 134
 135 definition pointwise_paths:
 136  ∀A:Type[0]. ∀P:A → Type[0]. ∀f,g: ∀x:A. P x. Type[0] ≝
 137  λA,P,f,g. ∀x. f x = g x.
 138
 139 interpretation "pointwise_paths" 'congruent f g T = (pointwise_paths ? T f g).
 140
 141 definition apD10: ∀A:Type[0]. ∀B:A→Type[0]. ∀f,g: ∀x. B x. f = g → f ≅ g.
 142  #A #B #f #g * #x %
 143 qed.
 144
 145 definition ap10: ∀A,B: Type[0]. ∀f,g:A → B. f=g → f ≅ g ≝
 146  λA,B,f. apD10 … f.
 147
 148 definition ap11: ∀A,B: Type[0]. ∀f,g: A → B. f=g → ∀x,y:A. x=y → f x = g y.
 149  #A #B #f #g * #x #y * %
 150 qed.
 151
 152 (* * Similarly, dependent functions act on paths; but the type is a bit more
 153   subtle. If [f : forall a:A, B a] and [p : x = y] is a path in [A], then
 154   [apD f p] should somehow be a path between [f x : B x] and [f y : B y].
 155   Since these live in different types, we use transport along [p] to make them
 156   comparable: [apD f p : p # f x = f y].
 157
 158   The type [p # f x = f y] can profitably be considered as a heterogeneous or
 159   dependent equality type, of "paths from [f x] to [f y] over [p]". *)
 160
 161 definition apD:
 162  ∀A:Type[0]. ∀B:A → Type[0]. ∀f:∀a:A. B a. ∀x,y:A.
 163    ∀p:x=y. p # (f x) = f y.
 164  #A #B #f #x #y * %
 165 qed.
 166
 167 (* * ** Equivalences *)
 168
 169 (* * Homotopy equivalences are a central concept in homotopy type theory.
 170   Before we define equivalences, let us consider when two types [A] and [B]
 171   should be considered "the same".
 172
 173   The first option is to require existence of [f : A -> B] and [g : B -> A]
 174   which are inverses of each other, up to homotopy. Homotopically speaking, we
 175   should also require a certain condition on these homotopies, which is one of
 176   the triangle identities for adjunctions in category theory.  Thus, we call
 177   this notion an *adjoint equivalence*.
 178
 179   The other triangle identity is provable from the first one, along with all the
 180   higher coherences, so it is reasonable to only assume one of them.  Moreover,
 181   as we will see, if we have maps which are inverses up to homotopy, it is always
 182   possible to make the triangle identity hold by modifying one of the homotopies.
 183
 184   The second option is to use Vladimir Voevodsky's definition of an equivalence
 185   as a map whose homotopy fibers are contractible.  We call this notion a
 186   *homotopy bijection*.
 187
 188   An interesting third option was suggested by André Joyal: a map [f] which has
 189   separate left and right homotopy inverses.  We call this notion a
 190   *homotopy isomorphism*.
 191
 192   While the second option was the one used originally, and it is the most
 193   concise one, it makes more sense to use the first one in a formalized
 194   development, since it exposes most directly equivalence as a structure.
 195   In particular, it is easier to extract directly from it the data of a homotopy
 196   inverse to [f], which is what we care about having most in practice.  Thus,
 197   adjoint equivalences are what we will refer to merely as *equivalences*. *)
 198
 199 (* * Naming convention: we use [equiv] and [Equiv] systematically to denote types
 200   of equivalences, and [isequiv] and [IsEquiv] systematically to denote the
 201   assertion that a given map is an equivalence. *)
 202
 203 (* * The fact that [r] is a left inverse of [s]. As a mnemonic, note that the
 204   partially applied type [Sect s] is the type of proofs that [s] is a section. *)
 205 definition Sect: ∀A,B : Type[0]. (A → B) → (B → A) → Type[0] ≝
 206  λA,B,s,r. ∀x : A. r (s x) = x.
 207
 208 (* * A typeclass that includes the data making [f] into an adjoint equivalence. *)
 209 record IsEquiv (A,B : Type[0]) (f : A → B) : Type[0] ≝ {
 210   equiv_inv : B → A ;
 211   eisretr : Sect … equiv_inv f;
 212   eissect : Sect … f equiv_inv;
 213   eisadj : ∀x:A. eisretr (f x) = (* f (equiv_inv (f x)) = f x *) ap … f … (eissect x)
 214 }.
 215
 216 (* * A record that includes all the data of an adjoint equivalence. *)
 217 record Equiv (A,B) : Type[0] ≝ {
 218   equiv_fun :1> A → B ;
 219   equiv_isequiv :> IsEquiv … equiv_fun
 220 }.
 221
 222 interpretation "Equiv" 'equiv A B p = (Equiv A B).
 223
 224 (* * A notation for the inverse of an equivalence.  We can apply this to a
 225   function as long as there is a typeclass instance asserting it to be an
 226   equivalence.  We can also apply it to an element of [A <~> B], since there is
 227   an implicit coercion to [A -> B] and also an existing instance of [IsEquiv]. *)
 228
 229 (*CSC: PROBABLY WE NEED TO INTERPRET 'invert_appl TOO *)
 230 interpretation "equiv_inv" 'invert f = (equiv_inv ?? f ?).
 231
 232 (*
 233 (** ** Contractibility and truncation levels *)
 234
 235 (** Truncation measures how complicated a type is.  In this library, a witness that a type is n-truncated is formalized by the [IsTrunc n] typeclass.  In many cases, the typeclass machinery of Coq can automatically infer a witness for a type being n-truncated.  Because [IsTrunc n A] itself has no computational content (that is, all witnesses of n-truncation of a type are provably equal), it does not matter much which witness Coq infers.  Therefore, the primary concerns in making use of the typeclass machinery are coverage (how many goals can be automatically solved) and speed (how long does it take to solve a goal, and how long does it take to error on a goal we cannot automatically solve).  Careful use of typeclass instances and priorities, which determine the order of typeclass resolution, can be used to effectively increase both the coverage and the speed in cases where the goal is solvable.  Unfortunately, typeclass resolution tends to spin for a while before failing unless you're very, very, very careful.  We currently aim to achieve moderate coverage and fast speed in solvable cases.  How long it takes to fail typeclass resolution is not currently considered, though it would be nice someday to be even more careful about things.
 236
 237 In order to achieve moderate coverage and speedy resolution, we currently follow the following principles.  They set up a kind of directed flow of information, intended to prevent cycles and potentially infinite chains, which are often the ways that typeclass resolution gets stuck.
 238
 239 - We prefer to reason about [IsTrunc (S n) A] rather than [IsTrunc n (@paths A a b)].  Whenever we see a statement (or goal) about truncation of paths, we try to turn it into a statement (or goal) about truncation of a (non-[paths]) type.  We do not allow typeclass resolution to go in the reverse direction from [IsTrunc (S n) A] to [forall a b : A, IsTrunc n (a = b)].
 240
 241 - We prefer to reason about syntactically smaller types.  That is, typeclass instances should turn goals of type [IsTrunc n (forall a : A, P a)] into goals of type [forall a : A, IsTrunc n (P a)]; and goals of type [IsTrunc n (A * B)] into the pair of goals of type [IsTrunc n A] and [IsTrunc n B]; rather than the other way around.  Ideally, we would add similar rules to transform hypotheses in the cases where we can do so.  This rule is not always the one we want, but it seems to heuristically capture the shape of most cases that we want the typeclass machinery to automatically infer.  That is, we often want to infer [IsTrunc n (A * B)] from [IsTrunc n A] and [IsTrunc n B], but we (probably) don't often need to do other simple things with [IsTrunc n (A * B)] which are broken by that reduction.
 242 *)
 243
 244 (** *** Contractibility *)
 245
 246 (** A space [A] is contractible if there is a point [x : A] and a (pointwise) homotopy connecting the identity on [A] to the constant map at [x].  Thus an element of [contr A] is a pair whose first component is a point [x] and the second component is a pointwise retraction of [A] to [x]. *)
 247
 248 (** We use the [Contr_internal] record so as not to pollute typeclass search; we only do truncation typeclass search on the [IsTrunc] datatype, usually.  We will define a notation [Contr] which is equivalent to [Contr_internal], but picked up by typeclass search.  However, we must make [Contr_internal] a class so that we pick up typeclasses on [center] and [contr].  However, the only typeclass rule we register is the one that turns it into a [Contr]/[IsTrunc].  Unfortunately, this means that declaring an instance like [Instance contr_foo : Contr foo := { center := bar }.] will fail with mismatched instances/contexts.  Instead, we must iota expand such definitions to get around Coq's deficiencies, and write [Instance contr_foo : Contr foo := let x := {| center := bar |} in x.] *)
 249 Class Contr_internal (A : Type) := BuildContr {
 250   center : A ;
 251   contr : (forall y : A, center = y)
 252 }.
 253
 254 Arguments center A {_}.
 255
 256 (** *** Truncation levels *)
 257
 258 (** Truncation measures how complicated a type is in terms of higher path spaces. The (-2)-truncated types are the contractible ones, whose homotopy is completely trivial. The (n+1)-truncated types are those whose path spaces are n-truncated.
 259
 260    Thus, (-1)-truncated means "the space of paths between any two points is contactible". Such a space is necessarily a sub-singleton: any two points are connected by a path which is unique up to homotopy. In other words, (-1)-truncated spaces are truth values (we call them "propositions").
 261
 262    Next, 0-truncated means "the space of paths between any two points is a sub-singleton". Thus, two points might not have any paths between them, or they have a unique path. Such a space may have many points but it is discrete in the sense that all paths are trivial. We call such spaces "sets".
 263 *)
 264
 265 Inductive trunc_index : Type :=
 266 | minus_two : trunc_index
 267 | trunc_S : trunc_index -> trunc_index.
 268
 269 (** We will use [Notation] for [trunc_index]es, so define a scope for them here. *)
 270 Delimit Scope trunc_scope with trunc.
 271 Bind Scope trunc_scope with trunc_index.
 272 Arguments trunc_S _%trunc_scope.
 273
 274 Fixpoint nat_to_trunc_index (n : nat) : trunc_index
 275   := match n with
 276        | 0 => trunc_S (trunc_S minus_two)
 277        | S n' => trunc_S (nat_to_trunc_index n')
 278      end.
 279
 280 Coercion nat_to_trunc_index : nat >-> trunc_index.
 281
 282 Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
 283   match n with
 284     | minus_two => Contr_internal A
 285     | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
 286   end.
 287
 288 Notation minus_one:=(trunc_S minus_two).
 289 (** Include the basic numerals, so we don't need to go through the coercion from [nat], and so that we get the right binding with [trunc_scope]. *)
 290 Notation "0" := (trunc_S minus_one) : trunc_scope.
 291 Notation "1" := (trunc_S 0) : trunc_scope.
 292 Notation "2" := (trunc_S 1) : trunc_scope.
 293
 294 Arguments IsTrunc_internal n A : simpl nomatch.
 295
 296 Class IsTrunc (n : trunc_index) (A : Type) : Type :=
 297   Trunc_is_trunc : IsTrunc_internal n A.
 298
 299 (** We use the priciple that we should always be doing typeclass resolution on truncation of non-equality types.  We try to change the hypotheses and goals so that they never mention something like [IsTrunc n (_ = _)] and instead say [IsTrunc (S n) _].  If you're evil enough that some of your paths [a = b] are n-truncated, but others are not, then you'll have to either reason manually or add some (local) hints with higher priority than the hint below, or generalize your equality type so that it's not a path anymore. *)
 300
 301 Typeclasses Opaque IsTrunc. (* don't auto-unfold [IsTrunc] in typeclass search *)
 302
 303 Arguments IsTrunc : simpl never. (* don't auto-unfold [IsTrunc] with [simpl] *)
 304
 305 Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A)
 306 : IsTrunc n (x = y)
 307   := H x y. (* but do fold [IsTrunc] *)
 308
 309 Hint Extern 0 => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *)
 310
 311 (** Picking up the [forall x y, IsTrunc n (x = y)] instances in the hypotheses is much tricker.  We could do something evil where we declare an empty typeclass like [IsTruncSimplification] and use the typeclass as a proxy for allowing typeclass machinery to factor nested [forall]s into the [IsTrunc] via backward reasoning on the type of the hypothesis... but, that's rather complicated, so we instead explicitly list out a few common cases.  It should be clear how to extend the pattern. *)
 312 Hint Extern 10 =>
 313 progress match goal with
 314            | [ H : forall x y : ?T, IsTrunc ?n (x = y) |- _ ]
 315              => change (IsTrunc (trunc_S n) T) in H
 316            | [ H : forall (a : ?A) (x y : @?T a), IsTrunc ?n (x = y) |- _ ]
 317              => change (forall a : A, IsTrunc (trunc_S n) (T a)) in H; cbv beta in H
 318            | [ H : forall (a : ?A) (b : @?B a) (x y : @?T a b), IsTrunc ?n (x = y) |- _ ]
 319              => change (forall (a : A) (b : B a), IsTrunc (trunc_S n) (T a b)) in H; cbv beta in H
 320            | [ H : forall (a : ?A) (b : @?B a) (c : @?C a b) (x y : @?T a b c), IsTrunc ?n (x = y) |- _ ]
 321              => change (forall (a : A) (b : B a) (c : C a b), IsTrunc (trunc_S n) (T a b c)) in H; cbv beta in H
 322            | [ H : forall (a : ?A) (b : @?B a) (c : @?C a b) (d : @?D a b c) (x y : @?T a b c d), IsTrunc ?n (x = y) |- _ ]
 323              => change (forall (a : A) (b : B a) (c : C a b) (d : D a b c), IsTrunc (trunc_S n) (T a b c d)) in H; cbv beta in H
 324          end.
 325
 326 Notation Contr := (IsTrunc minus_two).
 327 Notation IsHProp := (IsTrunc minus_one).
 328 Notation IsHSet := (IsTrunc 0).
 329
 330 Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
 331
 332 (** *** Function extensionality *)
 333
 334 (** The function extensionality axiom is formulated as a class. To use it in a theorem, just assume it with [`{Funext}], and then you can use [path_forall], defined below.  If you need function extensionality for a whole development, you can assume it for an entire Section with [Context `{Funext}].  *)
 335 Class Funext :=
 336   { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
 337
 338 Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
 339   f == g -> f = g
 340   :=
 341   (@apD10 A P f g)^-1.
 342
 343 Definition path_forall2 `{Funext} {A B : Type} {P : A -> B -> Type} (f g : forall x y, P x y) :
 344   (forall x y, f x y = g x y) -> f = g
 345   :=
 346   (fun E => path_forall f g (fun x => path_forall (f x) (g x) (E x))).
 347
 348
 349 (** *** Tactics *)
 350
 351 (** We declare some more [Hint Resolve] hints, now in the "hint database" [path_hints].  In general various hints (resolve, rewrite, unfold hints) can be grouped into "databases". This is necessary as sometimes different kinds of hints cannot be mixed, for example because they would cause a combinatorial explosion or rewriting cycles.
 352
 353    A specific [Hint Resolve] database [db] can be used with [auto with db].
 354
 355    The hints in [path_hints] are designed to push concatenation *outwards*, eliminate identities and inverses, and associate to the left as far as  possible. *)
 356
 357 (** TODO: think more carefully about this.  Perhaps associating to the right would be more convenient? *)
 358 Hint Resolve
 359   @idpath @inverse
 360  : path_hints.
 361
 362 Hint Resolve @idpath : core.
 363
 364 Ltac path_via mid :=
 365   apply @concat with (y := mid); auto with path_hints.
 366
 367 (** We put [Empty] here, instead of in [Empty.v], because [Ltac done] uses it. *)
 368 Inductive Empty : Type := .
 369
 370 Definition not (A:Type) : Type := A -> Empty.
 371 Notation "~ x" := (not x) : type_scope.
 372 Hint Unfold not: core.
 373
 374 (** *** Pointed types *)
 375
 376 (** A space is pointed if that space has a point. *)
 377 Class IsPointed (A : Type) := point : A.
 378 Definition pointedType := { u : Type & IsPointed u }.
 379
 380 (** Ssreflect tactics, adapted by Robbert Krebbers *)
 381 Ltac done :=
 382   trivial; intros; solve
 383     [ repeat first
 384       [ solve [trivial]
 385       | solve [eapply symmetry; trivial]
 386       | reflexivity
 387       (* Discriminate should be here, but it doesn't work yet *)
 388       (* | discriminate *)
 389       | contradiction
 390       | split ]
 391     | match goal with
 392       H : ~ _ |- _ => solve [destruct H; trivial]
 393       end ].
 394 Tactic Notation "by" tactic(tac) :=
 395   tac; done.
 396
 397 (** A convenient tactic for using function extensionality. *)
 398 Ltac by_extensionality x :=
 399   intros; unfold compose;
 400   match goal with
 401   | [ |- ?f = ?g ] => eapply path_forall; intro x;
 402       match goal with
 403         | [ |- forall (_ : prod _ _), _ ] => intros [? ?]
 404         | [ |- forall (_ : sigT _ _), _ ] => intros [? ?]
 405         | _ => intros
 406     end;
 407     simpl; auto with path_hints
 408   end.
 409
 410 (** Removed auto. We can write "by (path_induction;auto with path_hints)"
 411  if we want to.*)
 412 Ltac path_induction :=
 413   intros; repeat progress (
 414     match goal with
 415       | [ p : _ = _  |- _ ] => induction p
 416       | _ => idtac
 417     end
 418   ).
 419
 420 (** The tactic [f_ap] is a replacement for the previously existing standard library tactic [f_equal].  This tactic works by repeatedly applying the fact that [f = g -> x = y -> f x = g y] to turn, e.g., [f x y = f z w] first into [f x = f z] and [y = w], and then turns the first of these into [f = f] and [x = z].  The [done] tactic is used to detect the [f = f] case and finish, and the [trivial] is used to solve, e.g., [x = x] when using [f_ap] on [f y x = f z x].  This tactic only works for non-dependently-typed functions; we cannot express [y = w] in the first example if [y] and [w] have different types.  If and when Arnaud's new-tacticals branch lands, and we can have a goal which depends on the term used to discharge another goal, then this tactic should probably be generalized to deal with dependent functions. *)
 421 Ltac f_ap :=
 422   lazymatch goal with
 423     | [ |- ?f ?x = ?g ?x ] => apply (@apD10 _ _ f g);
 424                              try (done || f_ap)
 425     | _ => apply ap11;
 426           [ done || f_ap
 427           | trivial ]
 428   end.
 429
 430 (** [expand] replaces both terms of an equality (either [paths] or [pointwise_paths] in the goal with their head normal forms *)
 431 Ltac expand :=
 432   match goal with
 433     | [ |- ?X = ?Y ] =>
 434       let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' = Y')
 435     | [ |- ?X == ?Y ] =>
 436       let X' := eval hnf in X in let Y' := eval hnf in Y in change (X' == Y')
 437   end; simpl.
 438
 439 (** [atomic x] is the same as [idtac] if [x] is a variable or hypothesis, but is [fail 0] if [x] has internal structure. *)
 440 Ltac atomic x :=
 441   match x with
 442     | ?f _ => fail 1 x "is not atomic"
 443     | (fun _ => _) => fail 1 x "is not atomic"
 444     | forall _, _ => fail 1 x "is not atomic"
 445     | _ => idtac
 446   end.
 447 *)