]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/hott/Overture.ma
- cprs and cnx on the way
[helm.git] / matita / matita / lib / hott / Overture.ma
1 include "hott/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 *)