X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=d6043fba2c1d413fc22626fd567e18dbc34c5779;hb=a8285ad2e16e571100a666bc9178347d9e61dbe5;hp=e98696589e2f30f48fdfa9011a8df7c1c2692285;hpb=7e035682056388e730f03e214774d093e06ef650;p=helm.git diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index e98696589..d6043fba2 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -1,7 +1,7 @@ (*D -Matita Tutorial: inductively generated formal topologies -======================================================== +Inductively generated formal topologies in Matita +================================================= This is a not so short introduction to [Matita][2], based on the formalization of the paper @@ -11,16 +11,31 @@ the formalization of the paper > inductive generation of formal topologies by Stefano Berardi and Silvio Valentini. -The tutorial is by Enrico Tassi. -The tutorial spends a considerable amount of effort in defining +The tutorial and the formalization are by Enrico Tassi. + +The reader should be familiar with inductively generated +formal topologies and have some basic knowledge of type theory and λ-calculus. + +A considerable part of this tutorial is devoted to explain how to define notations that resemble the ones used in the original paper. We believe -this is a important part of every formalization, not only from the aesthetic +this is an important part of every formalization, not only from the aesthetic point of view, but also from the practical point of view. Being consistent allows to follow the paper in a pedantic way, and hopefully to make the formalization (at least the definitions and proved statements) readable to the author of the paper. +The formalization uses the "new generation" version of Matita +(that will be named 1.x when finally released). +Last stable release of the "old" system is named 0.5.7; the ng system +is coexisting with the old one in all development release +(named "nightly builds" in the download page of Matita) +with a version strictly greater than 0.5.7. + +To read this tutorial in HTML format, you need a decent browser +equipped with a unicode capable font. Use the PDF format if some +symbols are not displayed correctly. + Orienteering ------------ @@ -72,6 +87,11 @@ implements two unusual input facilities: example W has Ω, ð and ð, L has Î, ð, and ð, F has Φ, ⦠Variants are listed in the aforementioned TeX/UTF-8 table. +The syntax of terms (and types) is the one of the λ-calculus CIC +on which Matita is based. The main syntactical difference w.r.t. +the usual mathematical notation is the function application, written +`(f x y)` in place of `f(x,y)`. + Pressing `F1` opens the Matita manual. CIC (as [implemented in Matita][3]) in a nutshell @@ -95,9 +115,7 @@ of output). The CIC λ-calculus is equipped with a pattern matching construct (match) on inductive types defined in the environment. This construct, together with the possibility to definable total recursive functions, allows to define eliminators (or constructors) -for (co)inductive types. The λ-calculus is also equipped with explicitly typed -local definitions (let in) that in the degenerate case work as casts (i.e. -the type annotation `(t : T)` is implemented as `let x : T â t in x`). +for (co)inductive types. Types are compare up to conversion. Since types may depend on terms, conversion involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local @@ -108,11 +126,7 @@ computation). Since we are going to formalize constructive and predicative mathematics in an intensional type theory like CIC, we try to establish some terminology. Type is the sort of sets equipped with the `Id` equality (i.e. an intensional, -not quotiented set). We will avoid using `Id` (Leibniz equality), -thus we will explicitly equip a set with an equivalence relation when needed. -We will call this structure a _setoid_. Note that we will -attach the infix `=` symbol only to the equality of a setoid, -not to Id. +not quotiented set). We write `Type[i]` to mention a Type in the predicative hierarchy of types. To ease the comprehension we will use `Type[0]` for sets, @@ -121,12 +135,112 @@ universes are declared by the user. The standard library defines > Type[0] < Type[1] < Type[2] +Matita implements a variant of CIC in which constructive and predicative proposition +are distinguished from predicative data types. + + + For every `Type[i]` there is a corresponding level of predicative -propositions `CProp[i]`. A predicative proposition cannot be eliminated toward -`Type[j]` unless it holds no computational content (i.e. it is an inductive type +propositions `CProp[i]` (the C initial is due to historical reasons, and +stands for constructive). +A predicative proposition cannot be eliminated toward +`Type[j]` unless it holds no computational content (i.e. it is an inductive proposition with 0 or 1 constructors with propositional arguments, like `Id` and `And` but not like `Or`). +The distinction between predicative propositions and predicative data types +is a peculiarity of Matita (for example in CIC as implemented by Coq they are the +same). The additional restriction of not allowing the elimination of a CProp +toward a Type makes the theory of Matita minimal in the following sense: + + + +Theorems proved in CIC as implemented in Matita can be reused in a classical +and impredicative framework (i.e. forcing Matita to collapse the hierarchy of +constructive propositions and assuming the excluded middle on them). +Alternatively, one can decide to collapse predicative propositions and +predicative data types recovering the Axiom of Choice in the sense of Martin Löf +(i.e. â really holds a witness and can be eliminated to inhabit a type). + +This implementation of CIC is the result of the collaboration with Maietti M., +Sambin G. and Valentini S. of the University of Padua. + +Formalization choices +--------------------- + +There are many different ways of formalizing the same piece of mathematics +in CIC, depending on what our interests are. There is usually a trade-off +between the possibility of reuse the formalization we did and its complexity. + +In this work, our decisions mainly regarded the following two areas + +- Axiom of Choice: controlled use or not +- Equality: Id or not + +### Axiom of Choice + +In this paper it is clear that the author is interested in using the Axiom +of Choice, thus choosing to identify â and Σ (i.e. working in the +leftmost box of the graph "Coq's CIC (work in CProp)") would be a safe decision +(that is, the author of the paper would not complain we formalized something +different from what he had in mind). + +Anyway, we may benefit from the minimality of CIC as implemented in Matita, +"asking" the type system to ensure we do no use the Axiom of Choice elsewhere +in the proof (by mistake or as a shortcut). If we identify â and Σ from the +very beginning, the system will not complain if we use the Axiom of Choice at all. +Moreover, the elimination of an inductive type (like â) is a so common operation +that the syntax chosen for the elimination command is very compact and non +informative, hard to spot for a human being +(in fact it is just two characters long!). + +We decided to formalize the whole paper without identifying +CProp and Type and assuming the Axiom of Choice as a real axiom +(i.e. a black hole with no computational content, a function with no body). + +It is clear that this approach give us full control on when/where we really use +the Axiom of Choice. But, what are we loosing? What happens to the computational +content of the proofs if the Axiom of Choice gives no content back? + +It really +depends on when we actually look at the computational content of the proof and +we "run" that program. We can extract the content and run it before or after +informing the system that our propositions are actually code (i.e. identifying +â and Σ). If we run the program before, as soon as the computation reaches the +Axiom of Choice it stops, giving no output. If we tell the system that CProp and +Type are the same, we can exhibit a body for the Axiom of Choice (i.e. a projection) +and the extracted code would compute an output. + +Note that the computational +content is there even if the Axiom of Choice is an axiom, the difference is +just that we cannot use it (the typing rules inhibit the elimination of the +existential). This is possible only thanks to the minimality of CIC as implemented +in Matita. + +### Equality + +What we have to decide here is which models we admit. The paper does not +mention quotiented sets, thus using an intensional equality is enough +to capture the intended content of the paper. Nevertheless, the formalization +cannot be reused in a concrete example where the (families of) sets +that will build the axiom set are quotiented. + +Matita gives support for setoid rewriting under a context built with +non dependent morphisms. As we will detail later, if we assume a generic +equality over the carrier of our axiom set, a non trivial inductive +construction over the ordinals has to be proved to respect extensionality +(i.e. if the input is an extensional set, also the output is). +The proof requires to rewrite under the context formed by the family of sets +`I` and `D`, that have a dependent type. Declaring them as dependently typed +morphisms is possible, but Matita does not provide an adequate support for them, +and would thus need more effort than formalizing the whole paper. + +Anyway, in a preliminary attempt of formalization, we tried the setoid approach, +reaching the end of the formalization, but we had to assume the proof +of the extensionality of the `U_x` construction (while there is no +need to assume the same property for `F_x`!). + +The current version of the formalization uses `Id`. The standard library and the `include` command ---------------------------------------------- @@ -159,7 +273,7 @@ Some basic results that we will use are also part of the sets library: Defining Axiom set ------------------ -A set of axioms is made of a set(oid) `S`, a family of sets `I` and a +A set of axioms is made of a set `S`, a family of sets `I` and a family `C` of subsets of `S` indexed by elements `a` of `S` and elements of `I(a)`. @@ -175,9 +289,9 @@ with `C A`. D*) nrecord Ax : Type[1] â { - S :> setoid; + S :> Type[0]; I : S â Type[0]; - C : âa:S. I a â Ω ^ S + C : âa:S. I a â Ω^S }. (*D @@ -187,13 +301,6 @@ the record definition. It is made of a list of pairs: a name, followed by `:` and the its type. It is a dependently typed tuple, thus already defined names (fields) can be used in the types that follow. -Note that `S` is declared to be a `setoid` and not a Type. The original -paper probably also considers I to generate setoids, and both I and C -to be (dependent) morphisms. For the sake of simplicity, we will "cheat" and use -setoids only when strictly needed (i.e. where we want to talk about -equality). Setoids will play a role only when we will define -the alternative version of the axiom set. - Note that the field `S` was declared with `:>` instead of a simple `:`. This declares the `S` projection to be a coercion. A coercion is a "cast" function the system automatically inserts when it is needed. @@ -332,6 +439,10 @@ has to notice that the infinity rule uses, in its hypotheses, the cover relation between two subsets, while the inductive predicate we are going to define relates an element and a subset. + a â U i â I(a) C(a,i) â U + (reflexivity) â¼â¼â¼â¼â¼â¼â¼â¼â¼ (infinity) â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼ + a â U a â U + An option would be to unfold the definition of cover between subsets, but we prefer to define the abstract notion of cover between subsets (so that we can attach a (ambiguous) notation to it). @@ -364,6 +475,12 @@ but under the assumption that (for every y) `y â U`. In that rule, the left had side of the predicate changes, thus it has to be abstracted (in the arity of the inductive predicate) on the right of `:`. +The intuition Valentini suggests is that we are defining the unary predicate +"being covered by U" (i.e. `_ â U`) and not "being covered" (i.e. `_ â _`). +Unluckily, the syntax of Matita forces us to abstract `U` first, and +we will make it the second argument of the predicate using +the notational support Matita offers. + D*) (** ncheck xcreflexivity. *) (* shows: âA:Ax.âU:Ω^A.âa:A.aâU â xcover A U a *) @@ -423,8 +540,8 @@ the premise of infinity. D*) ninductive cover (A : Ax) (U : Ω^A) : A â CProp[0] â -| creflexivity : âa. a â U â cover ? U a -| cinfinity : âa. âi. ð a i â U â cover ? U a. +| creflexivity : âa. a â U â cover A U a +| cinfinity : âa. âi. ð a i â U â cover A U a. (** screenshot "cover". *) napply cover; nqed. @@ -539,15 +656,19 @@ interpretation "fish" 'fish a U = (fish ? U a). Introduction rule for fish --------------------------- -Matita is able to generate elimination rules for inductive types, -but not introduction rules for the coinductive case. - +Matita is able to generate elimination rules for inductive types D*) (** ncheck cover_rect_CProp0. *) (*D +but not introduction rules for the coinductive case. + + P â U (âx,j.x â P â C(x,j) ⬠P) a â P + (fish intro) â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼ + a â U + We thus have to define the introduction rule for fish by co-recursion. Here we again use the proof mode of Matita to exhibit the body of the corecursive function. @@ -558,11 +679,11 @@ nlet corec fish_rec (A:Ax) (U: Ω^A) (P: Ω^A) (H1: P â U) (H2: âa:A. a â P â âj: ð a. ð a j ⬠P): âa:A. âp: a â P. a â U â ?. (** screenshot "def-fish-rec-1". *) -#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *) +#a; #a_in_P; napply cfish; (** screenshot "def-fish-rec-2". *) ##[ nchange in H1 with (âb.bâP â bâU); (** screenshot "def-fish-rec-2-1". *) napply H1; (** screenshot "def-fish-rec-3". *) nassumption; -##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *) +##| #i; ncases (H2 a a_in_P i); (** screenshot "def-fish-rec-5". *) #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *) @; (** screenshot "def-fish-rec-6". *) ##[ napply x @@ -620,7 +741,7 @@ In CIC it is a defined notion, that is an inductive type with just one constructor (one introduction rule) holding the witness and the proof that the witness satisfies a proposition. -> ncheck Ex. +> ncheck Ex. Instead of trying to remember the name of the constructor, that should be used as the argument of `napply`, we can ask the system to find by @@ -739,8 +860,8 @@ in the new definition of the axiom set with `n`. D*) -nrecord nAx : Type[2] â { - nS:> setoid; +nrecord nAx : Type[1] â { + nS:> Type[0]; nI: nS â Type[0]; nD: âa:nS. nI a â Type[0]; nd: âa:nS. âi:nI a. nD a i â nS @@ -790,8 +911,9 @@ form a subset, i.e. to place a single variable `{ here | ⦠}` of type `S`. > Im[d(a,i)] = { y | âj:D(a,i). y = d(a,i,j) } -This poses no theoretical problems, since `S` is a setoid and thus equipped -with an equality. +This poses no theoretical problems, since `S` is a Type and thus +equipped with the `Id` equality. If `S` was a setoid, here the equality +would have been the one of the setoid. Unless we define two different images, one for stating that the image is â of something and another one to define `ð`, we end up using always the latter. @@ -799,13 +921,24 @@ Thus the statement `Im[d(a,i)] â V` unfolds to > âx:S. ( âj.x = d(a,i,j) ) â x â V -That, up to rewriting with the equation defining `x`, is what we mean. -The technical problem arises later, when `V` will be a complex -construction that has to be proved extensional -(i.e. âx,y. x = y â x â V â y â V). +That, up to rewriting with the equation defining `x`, is what we mean. +Since we decided to use `Id` the rewriting always work (the elimination +principle for `Id` is Leibnitz's equality, that is quantified over +the context. + +The problem that arises if we decide to make `S` a setoid is that +`V` has to be extensional w.r.t. the equality of `S` (i.e. the characteristic +functional proposition has to quotient its input with a relation bigger +than the one of `S`. + +> âx,y:S. x = y â x â V â y â V + +If `V` is a complex construction, the proof may not be trivial. D*) +include "logic/equality.ma". + ndefinition image â λA:nAx.λa:A.λi. { x | âj:ð a i. x = ð a i j }. notation > "ðð¦ [ð term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }. @@ -836,6 +969,65 @@ nqed. (*D +We now prove that the two function above form a retraction pair for +the `C` component of the axiom set. To prove that we face a little +problem since CIC is not equipped with η-conversion. This means that +the followin does not hold (where `A` is an axiom set). + +> A = (S A, I A, C A) + +This can be proved only under a pattern mach over `A`, that means +that the resulting computation content of the proof is a program +that computes something only if `A` is a concrete axiom set. + +To state the lemma we have to drop notation, and explicitly +give the axiom set in input to the `C` projection. + +D*) + +nlemma Ax_nAx_equiv : + âA:Ax. âa,i. C (Ax_of_nAx (nAx_of_Ax A)) a i â C A a i ⧠+ C A a i â C (Ax_of_nAx (nAx_of_Ax A)) a i. +#A; #a; #i; @; #b; #H; (** screenshot "retr-1". *) +##[ ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H;(** screenshot "retr-2". *) + nchange in a with S; nwhd in H; (** screenshot "retr-3". *) + ncases H; #x; #E; nrewrite > E; nwhd in x; (** screenshot "retr-4". *) + ncases x; #b; #Hb; nnormalize; nassumption; +##| ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @; + ##[ @ b; nassumption; + ##| nnormalize; @; ##] +##] +nqed. + +(*D +D[retr-1] +Look for example the type of `a`. The command `nchange in a with A` +would fail because of the missing η-conversion rule. We have thus +to pattern match over `A` and introduce its pieces. + +D[retr-2] +Now the system accepts that the type of `a` is the fist component +of the axiom set, now called `S`. Unfolding definitions in `H` we discover +there is still some work to do. + +D[retr-3] +To use the equation defining `b` we have to eliminate `H`. Unfolding +definitions in `x` tell us there is still something to do. The `nrewrite` +tactic is a shortcut for the elimination principle of the equality. +It accepts an additional argument `<` or `>` to rewrite left-to-right +or right-to-left. + +D[retr-4] +We defined `ð` to be the first projection of `x`, thus we have to +eliminate `x` to actually compute `ð`. + +The remaining part of the proof it not interesting and poses no +new problems. + +D*) + +(*D + We then define the inductive type of ordinals, parametrized over an axiom set. We also attach some notations to the constructors. @@ -895,7 +1087,8 @@ of the tutorial works only for the old axiom set. D*) -ndefinition ord_coverage : âA:nAx.âU:Ω^A.Ω^A â λA,U.{ y | âx:Ord A. y â famU ? U x }. +ndefinition ord_coverage : âA:nAx.âU:Ω^A.Ω^A â + λA,U.{ y | âx:Ord A. y â famU ? U x }. ndefinition ord_cover_set â λc:âA:nAx.Ω^A â Ω^A.λA,C,U. ây.y â C â y â c A U. @@ -931,18 +1124,29 @@ naxiom AC : âA,a,i,U. (*D -In the proof of infinity, we have to rewrite under the â predicate. -It is clearly possible to show that `Uâ½x` is an extensional set: +Note that, if we will decide later to identify â and Σ, `AC` is +trivially provable + +D*) + +nlemma AC_exists_is_sigma : âA,a,i,U. + (âj:ð a i.Σx:Ord A.ð a i j â Uâ½x) â (Σf.âj:ð a i.ð a i j â Uâ½(f j)). +#A; #a; #i; #U; #H; @; +##[ #j; ncases (H j); #x; #_; napply x; +##| #j; ncases (H j); #x; #Hx; napply Hx; ##] +nqed. + +(*D + +In case we made `S` a setoid, the following property has to be proved -> a = b â a â Uâ½x â b â Uâ½x +> nlemma U_x_is_ext: âA:nAx.âa,b:A.âx.âU. a = b â b â Uâ½x â a â Uâ½x. Anyway this proof is a non trivial induction over x, that requires `ð` and `ð` to be -declared as morphisms. This poses no problem, but goes out of the scope of the -tutorial, since dependent morphisms are hard to manipulate, and we thus assume it. +declared as morphisms. D*) -naxiom U_x_is_ext: âA:nAx.âa,b:A.âx.âU. a = b â b â Uâ½x â a â Uâ½x. (*D @@ -964,21 +1168,20 @@ We now proceed with the proof of the infinity rule. D*) - -alias symbol "covers" = "new covers set". +alias symbol "covers" (instance 3) = "new covers set". ntheorem new_coverage_infinity: âA:nAx.âU:Ω^A.âa:A. (âi:ð a. ðð¦[ð a i] â U) â a â U. #A; #U; #a; (** screenshot "n-cov-inf-1". *) *; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *) ncut (ây:ð a i.âx:Ord A.ð a i y â Uâ½x); ##[ (** screenshot "n-cov-inf-3". *) - #z; napply H; @ z; napply #; ##] #H'; (** screenshot "n-cov-inf-4". *) + #z; napply H; @ z; @; ##] #H'; (** screenshot "n-cov-inf-4". *) ncases (AC ⦠H'); #f; #Hf; (** screenshot "n-cov-inf-5". *) ncut (âj.ð a i j â Uâ½(Î f)); ##[ #j; napply (ord_subset ⦠f ⦠(Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *) @ (Î f+1); (** screenshot "n-cov-inf-7". *) @2; (** screenshot "n-cov-inf-8". *) @i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *) -napply (U_x_is_ext ⦠Hd); napply Hf'; +nrewrite > Hd; napply Hf'; nqed. (*D @@ -996,8 +1199,7 @@ We thus assert (`ncut`) the nicer form of `H` and prove it. D[n-cov-inf-3] After introducing `z`, `H` can be applied (choosing `ð a i z` as `y`). What is the left to prove is that `âj: ð a j. ð a i z = ð a i j`, that -becomes trivial if `j` is chosen to be `z`. In the command `napply #`, -the `#` is a standard notation for the reflexivity property of the equality. +becomes trivial if `j` is chosen to be `z`. D[n-cov-inf-4] Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and @@ -1052,7 +1254,7 @@ nlemma new_coverage_min : *; #o; (** screenshot "n-cov-min-3". *) ngeneralize in match b; nchange with (Uâ½o â V); (** screenshot "n-cov-min-4". *) nelim o; (** screenshot "n-cov-min-5". *) -##[ #b; #bU0; napply HUV; napply bU0; +##[ napply HUV; ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##] #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans ⦠IH); napply H; ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##] @@ -1114,7 +1316,8 @@ We assume the dual of the axiom of choice, as in the paper proof. D*) naxiom AC_dual: âA:nAx.âa:A.âi,F. - (âf:ð a i â Ord A.âx:ð a i.ð a i x â Fâ½(f x)) â âj:ð a i.âx:Ord A.ð a i j â Fâ½x. + (âf:ð a i â Ord A.âx:ð a i.ð a i x â Fâ½(f x)) + â âj:ð a i.âx:Ord A.ð a i j â Fâ½x. (*D @@ -1182,12 +1385,9 @@ The proof that `â(F)` is maximal is exactly the dual one of the minimality of `â(U)`. Thus the main problem is to obtain `G â Fâ½o` before doing the induction over `o`. -Note that `G` is assumed to be of type `ð^A`, that means an extensional -subset of `S`, while `Ω^A` means just a subset (note that the former is bold). - D*) ntheorem max_new_fished: - âA:nAx.âG:ð^A.âF:Ω^A.G â F â (âa.a â G â âi.ðð¦[ð a i] ⬠G) â G â âF. + âA:nAx.âG:Ω^A.âF:Ω^A.G â F â (âa.a â G â âi.ðð¦[ð a i] ⬠G) â G â âF. #A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b; nchange with (G â Fâ½o); @@ -1195,45 +1395,22 @@ nelim o; ##[ napply GF; ##| #p; #IH; napply (subseteq_intersection_r ⦠IH); #x; #Hx; #i; ncases (H ⦠Hx i); #c; *; *; #d; #Ed; #cG; - @d; napply IH; (** screenshot "n-f-max-1". *) - alias symbol "prop2" = "prop21". - napply (. Ed^-1â¡#); napply cG; + @d; napply IH; (** screenshot "n-f-max-1". *) + nrewrite < Ed; napply cG; ##| #a; #i; #f; #Hf; nchange with (G â { y | âx. y â Fâ½(f x) }); #b; #Hb; #d; napply (Hf d); napply Hb; ##] nqed. -(*D -D[n-f-max-1] -Here the situation looks really similar to the one of the dual proof where -we had to apply the assumption `U_x_is_ext`, but here the set is just `G` -not `F_x`. Since we assumed `G` to be extensional we can -exploit the facilities -Matita provides to perform rewriting in the general setting of setoids. - -The `.` notation simply triggers the mechanism, while the given argument has to -mimic the context under which the rewriting has to happen. In that case -we want to rewrite the left hand side of the binary morphism `â`. -The infix notation -to represent the context of a binary morphism is `â¡`. The right hand side -has to be left untouched, and the identity rewriting step is represented with -`#` (actually a reflexivity proof for the subterm identified by the context). - -We want to rewrite the left hand side using `Ed` right-to-left (the default -is left-to-right). We thus write `Ed^-1`, that is a proof that `ð x i d = c`. - -The complete command is `napply (. Ed^-1â¡#)` that has to be read like: -> perform some rewritings under a binary morphism, -> on the right do nothing, -> on the left rewrite with Ed right-to-left. - -After the rewriting step the goal is exactly the `cG` assumption. - -D*) +(*D +D[n-f-max-1] +Note that here the right hand side of `â` is `G` and not `Fâ½p` as +in the dual proof. If `S` was declare to be a setoid, to finish this proof +would be enough to assume `G` extensional, and no proof of the +extensionality of `Fâ½p` is required. -(*D
Appendix: tactics explanation ----------------------------- @@ -1243,9 +1420,9 @@ in terms of sequent calculus rules annotated with proofs. The `:` separator has to be read as _is a proof of_, in the spirit of the Curry-Howard isomorphism. - Π⢠f : A1 â ⦠â An â B Π⢠?1 : A1 ⦠?n : An + Π⢠f : A_1 â ⦠â A_n â B Π⢠?_i : A_i napply f; â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼ - Π⢠(f ?1 ⦠?n ) : B + Π⢠(f ?_1 ⦠?_n ) : B Π⢠? : F â B Π⢠f : F nlapply f; â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼â¼