diff options
| -rw-r--r-- | doc/changelog/08-tools/10592-coqdoc-details.rst | 5 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/11946-ollibs-permutation.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/using/tools/coqdoc.rst | 21 | ||||
| -rw-r--r-- | theories/Sorting/Permutation.v | 287 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 25 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 22 | ||||
| -rw-r--r-- | tools/coqdoc/output.mli | 3 |
7 files changed, 369 insertions, 4 deletions
diff --git a/doc/changelog/08-tools/10592-coqdoc-details.rst b/doc/changelog/08-tools/10592-coqdoc-details.rst new file mode 100644 index 0000000000..c5bdc1dbb0 --- /dev/null +++ b/doc/changelog/08-tools/10592-coqdoc-details.rst @@ -0,0 +1,5 @@ +- **Added:** + A new documentation environment ``details`` to make certain portion + of a Coq document foldable. See :ref:`coqdoc` + (`#10592 <https://github.com/coq/coq/pull/10592>`_, + by Thomas Letan). diff --git a/doc/changelog/10-standard-library/11946-ollibs-permutation.rst b/doc/changelog/10-standard-library/11946-ollibs-permutation.rst new file mode 100644 index 0000000000..626677d31a --- /dev/null +++ b/doc/changelog/10-standard-library/11946-ollibs-permutation.rst @@ -0,0 +1,10 @@ +- **Added:** + Facts about ``Permutation``: + + - structure: ``Permutation_refl'``, ``Permutation_morph_transp`` + - compatibilities: ``Permutation_app_rot``, ``Permutation_app_swap_app``, ``Permutation_app_middle``, ``Permutation_middle2``, ``Permutation_elt``, ``Permutation_Forall``, ``Permutation_Exists``, ``Permutation_Forall2``, ``Permutation_flat_map``, ``Permutation_list_sum``, ``Permutation_list_max`` + - inversions: ``Permutation_app_inv_m``, ``Permutation_vs_elt_inv``, ``Permutation_vs_cons_inv``, ``Permutation_vs_cons_cons_inv``, ``Permutation_map_inv``, ``Permutation_image``, ``Permutation_elt_map_inv`` + - length-preserving definition by means of transpositions ``Permutation_transp`` with associated properties: ``Permutation_transp_sym``, ``Permutation_transp_equiv``, ``Permutation_transp_cons``, ``Permutation_Permutation_transp``, ``Permutation_ind_transp`` + + (`#11946 <https://github.com/coq/coq/pull/11946>`_, + by Olivier Laurent). diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index cada680895..b4b14fb392 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -248,6 +248,27 @@ shown using such comments: The latter cannot be used around some inner parts of a proof, but can be used around a whole proof. +Lastly, it is possible to adopt a middle-ground approach when the +desired output is HTML, where a given snippet of Coq material is +hidden by default, but can be made visible with user interaction. + +:: + + + (* begin details *) + *some Coq material* + (* end details *) + + +There is also an alternative syntax available. + +:: + + + (* begin details : Some summary describing the snippet *) + *some Coq material* + (* end details *) + Usage ~~~~~ diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 23881f63cb..86eebc6b4f 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -15,7 +15,7 @@ (* Adapted in May 2006 by Jean-Marc Notin from initial contents by Laurent Théry (Huffmann contribution, October 2003) *) -Require Import List Setoid Compare_dec Morphisms FinFun. +Require Import List Setoid Compare_dec Morphisms FinFun PeanoNat. Import ListNotations. (* For notations [] and [a;b;c] *) Set Implicit Arguments. (* Set Universe Polymorphism. *) @@ -56,6 +56,11 @@ Proof. induction l; constructor. exact IHl. Qed. +Instance Permutation_refl' : Proper (Logic.eq ==> Permutation) id. +Proof. + intros x y Heq; rewrite Heq; apply Permutation_refl. +Qed. + Theorem Permutation_sym : forall l l' : list A, Permutation l l' -> Permutation l' l. Proof. @@ -87,15 +92,28 @@ Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := { Equivalence_Symmetric := @Permutation_sym A ; Equivalence_Transitive := @Permutation_trans A }. +Lemma Permutation_morph_transp A : forall P : list A -> Prop, + (forall a b l1 l2, P (l1 ++ a :: b :: l2) -> P (l1 ++ b :: a :: l2)) -> + Proper (@Permutation A ==> Basics.impl) P. +Proof. + intros P HT l1 l2 HP. + enough (forall l0, P (l0 ++ l1) -> P (l0 ++ l2)) as IH + by (intro; rewrite <- (app_nil_l l2); now apply (IH nil)). + induction HP; intuition. + rewrite <- (app_nil_l l'), app_comm_cons, app_assoc. + now apply IHHP; rewrite <- app_assoc. +Qed. + Instance Permutation_cons A : Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10. Proof. repeat intro; subst; auto using perm_skip. Qed. + Section Permutation_properties. -Variable A:Type. +Variable A B:Type. Implicit Types a b : A. Implicit Types l m : list A. @@ -168,6 +186,30 @@ Proof. Qed. Local Hint Resolve Permutation_app_comm : core. +Lemma Permutation_app_rot : forall l1 l2 l3: list A, + Permutation (l1 ++ l2 ++ l3) (l2 ++ l3 ++ l1). +Proof. + intros l1 l2 l3; now rewrite (app_assoc l2). +Qed. +Local Hint Resolve Permutation_app_rot : core. + +Lemma Permutation_app_swap_app : forall l1 l2 l3: list A, + Permutation (l1 ++ l2 ++ l3) (l2 ++ l1 ++ l3). +Proof. + intros. + rewrite 2 app_assoc. + apply Permutation_app_tail, Permutation_app_comm. +Qed. +Local Hint Resolve Permutation_app_swap_app : core. + +Lemma Permutation_app_middle : forall l l1 l2 l3 l4, + Permutation (l1 ++ l2) (l3 ++ l4) -> + Permutation (l1 ++ l ++ l2) (l3 ++ l ++ l4). +Proof. + intros l l1 l2 l3 l4 HP. + now rewrite Permutation_app_swap_app, HP, Permutation_app_swap_app. +Qed. + Theorem Permutation_cons_app : forall (l l1 l2:list A) a, Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2). Proof. @@ -190,6 +232,24 @@ Proof. Qed. Local Hint Resolve Permutation_middle : core. +Lemma Permutation_middle2 : forall l1 l2 l3 a b, + Permutation (a :: b :: l1 ++ l2 ++ l3) (l1 ++ a :: l2 ++ b :: l3). +Proof. + intros l1 l2 l3 a b. + apply Permutation_cons_app. + rewrite 2 app_assoc. + now apply Permutation_cons_app. +Qed. +Local Hint Resolve Permutation_middle2 : core. + +Lemma Permutation_elt : forall l1 l2 l1' l2' (a:A), + Permutation (l1 ++ l2) (l1' ++ l2') -> + Permutation (l1 ++ a :: l2) (l1' ++ a :: l2'). +Proof. + intros l1 l2 l1' l2' a HP. + transitivity (a :: l1 ++ l2); auto. +Qed. + Theorem Permutation_rev : forall (l : list A), Permutation l (rev l). Proof. induction l as [| x l]; simpl; trivial. now rewrite IHl at 1. @@ -213,6 +273,46 @@ Proof. exact Permutation_length. Qed. +Instance Permutation_Forall (P : A -> Prop) : + Proper ((@Permutation A) ==> Basics.impl) (Forall P). +Proof. + intros l1 l2 HP. + induction HP; intro HF; auto. + - inversion_clear HF; auto. + - inversion_clear HF as [ | ? ? HF1 HF2]. + inversion_clear HF2; auto. +Qed. + +Instance Permutation_Exists (P : A -> Prop) : + Proper ((@Permutation A) ==> Basics.impl) (Exists P). +Proof. + intros l1 l2 HP. + induction HP; intro HF; auto. + - inversion_clear HF; auto. + - inversion_clear HF as [ | ? ? HF1 ]; auto. + inversion_clear HF1; auto. +Qed. + +Lemma Permutation_Forall2 (P : A -> B -> Prop) : + forall l1 l1' (l2 : list B), Permutation l1 l1' -> Forall2 P l1 l2 -> + exists l2' : list B, Permutation l2 l2' /\ Forall2 P l1' l2'. +Proof. + intros l1 l1' l2 HP. + revert l2; induction HP; intros l2 HF; inversion HF as [ | ? b ? ? HF1 HF2 ]; subst. + - now exists nil. + - apply IHHP in HF2 as [l2' [HP2 HF2]]. + exists (b :: l2'); auto. + - inversion_clear HF2 as [ | ? b' ? l2' HF3 HF4 ]. + exists (b' :: b :: l2'); auto. + - apply Permutation_nil in HP1; subst. + apply Permutation_nil in HP2; subst. + now exists nil. + - apply IHHP1 in HF as [l2' [HP2' HF2']]. + apply IHHP2 in HF2' as [l2'' [HP2'' HF2'']]. + exists l2''; split; auto. + now transitivity l2'. +Qed. + Theorem Permutation_ind_bis : forall P : list A -> list A -> Prop, P [] [] -> @@ -301,6 +401,16 @@ Proof. rewrite 2 (Permutation_app_comm _ l). apply Permutation_app_inv_l. Qed. +Lemma Permutation_app_inv_m l l1 l2 l3 l4 : + Permutation (l1 ++ l ++ l2) (l3 ++ l ++ l4) -> + Permutation (l1 ++ l2) (l3 ++ l4). +Proof. + intros HP. + apply (Permutation_app_inv_l l). + transitivity (l1 ++ l ++ l2); auto. + transitivity (l3 ++ l ++ l4); auto. +Qed. + Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a]. Proof. intros a l H; remember [a] as m in H. @@ -335,6 +445,38 @@ Proof. apply Permutation_length_2_inv in H as [H|H]; injection H as [= -> ->]; auto. Qed. +Lemma Permutation_vs_elt_inv : forall l l1 l2 a, + Permutation l (l1 ++ a :: l2) -> exists l' l'', l = l' ++ a :: l''. +Proof. + intros l l1 l2 a HP. + symmetry in HP. + apply (Permutation_in a), in_split in HP; trivial. + apply in_elt. +Qed. + +Lemma Permutation_vs_cons_inv : forall l l1 a, + Permutation l (a :: l1) -> exists l' l'', l = l' ++ a :: l''. +Proof. + intros l l1 a HP. + rewrite <- (app_nil_l (a :: l1)) in HP. + apply (Permutation_vs_elt_inv _ _ _ HP). +Qed. + +Lemma Permutation_vs_cons_cons_inv : forall l l' a b, + Permutation l (a :: b :: l') -> + exists l1 l2 l3, l = l1 ++ a :: l2 ++ b :: l3 \/ l = l1 ++ b :: l2 ++ a :: l3. +Proof. + intros l l' a b HP. + destruct (Permutation_vs_cons_inv HP) as [l1 [l2]]; subst. + symmetry in HP. + apply Permutation_cons_app_inv in HP. + apply (Permutation_in b), in_app_or in HP; [|now apply in_eq]. + destruct HP as [(l3 & l4 & ->)%in_split | (l3 & l4 & ->)%in_split]. + - exists l3, l4, l2; right. + now rewrite <-app_assoc; simpl. + - now exists l1, l3, l4; left. +Qed. + Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' -> (forall x:A, In x l <-> In x l') -> Permutation l l'. Proof. @@ -367,8 +509,8 @@ Qed. Lemma Permutation_NoDup l l' : Permutation l l' -> NoDup l -> NoDup l'. Proof. induction 1; auto. - * inversion_clear 1; constructor; eauto using Permutation_in. - * inversion_clear 1 as [|? ? H1 H2]. inversion_clear H2; simpl in *. + - inversion_clear 1; constructor; eauto using Permutation_in. + - inversion_clear 1 as [|? ? H1 H2]. inversion_clear H2; simpl in *. constructor. simpl; intuition. constructor; intuition. Qed. @@ -397,6 +539,63 @@ Proof. exact Permutation_map. Qed. +Lemma Permutation_map_inv : forall l1 l2, + Permutation l1 (map f l2) -> exists l3, l1 = map f l3 /\ Permutation l2 l3. +Proof. + induction l1; intros l2 HP. + - exists nil; split; auto. + apply Permutation_nil in HP. + destruct l2; auto. + inversion HP. + - symmetry in HP. + destruct (Permutation_vs_cons_inv HP) as [l3 [l4 Heq]]. + destruct (map_eq_app _ _ _ _ Heq) as [l1' [l2' [Heq1 [Heq2 Heq3]]]]; subst. + symmetry in Heq3. + destruct (map_eq_cons _ _ Heq3) as [b [l1'' [Heq1' [Heq2' Heq3']]]]; subst. + rewrite map_app in HP; simpl in HP. + symmetry in HP. + apply Permutation_cons_app_inv in HP. + rewrite <- map_app in HP. + destruct (IHl1 _ HP) as [l3 [Heq1'' Heq2'']]; subst. + exists (b :: l3); split; auto. + symmetry in Heq2''; symmetry; apply (Permutation_cons_app _ _ _ Heq2''). +Qed. + +Lemma Permutation_image : forall a l l', + Permutation (a :: l) (map f l') -> exists a', a = f a'. +Proof. + intros a l l' HP. + destruct (Permutation_map_inv _ HP) as [l'' [Heq _]]. + destruct l'' as [ | a' l'']; inversion_clear Heq. + now exists a'. +Qed. + +Lemma Permutation_elt_map_inv: forall l1 l2 l3 l4 a, + Permutation (l1 ++ a :: l2) (l3 ++ map f l4) -> (forall b, a <> f b) -> + exists l1' l2', l3 = l1' ++ a :: l2'. +Proof. + intros l1 l2 l3 l4 a HP Hf. + apply (Permutation_in a), in_app_or in HP; [| now apply in_elt]. + destruct HP as [HP%in_split | (x & Heq & ?)%in_map_iff]; trivial; subst. + now contradiction (Hf x). +Qed. + +Instance Permutation_flat_map (g : A -> list B) : + Proper ((@Permutation A) ==> (@Permutation B)) (flat_map g). +Proof. + intros l1; induction l1; intros l2 HP. + - now apply Permutation_nil in HP; subst. + - symmetry in HP. + destruct (Permutation_vs_cons_inv HP) as [l' [l'']]; subst. + symmetry in HP. + apply Permutation_cons_app_inv in HP. + rewrite flat_map_app; simpl. + rewrite <- (app_nil_l _). + apply Permutation_app_middle; simpl. + rewrite <- flat_map_app. + apply (IHl1 _ HP). +Qed. + End Permutation_map. Lemma nat_bijection_Permutation n f : @@ -573,6 +772,86 @@ Qed. End Permutation_alt. +Instance Permutation_list_sum : Proper (@Permutation nat ==> eq) list_sum. +Proof. + intros l1 l2 HP; induction HP; simpl; intuition. + - rewrite 2 (Nat.add_comm x). + apply Nat.add_assoc. + - now transitivity (list_sum l'). +Qed. + +Instance Permutation_list_max : Proper (@Permutation nat ==> eq) list_max. +Proof. + intros l1 l2 HP; induction HP; simpl; intuition. + - rewrite 2 (Nat.max_comm x). + apply Nat.max_assoc. + - now transitivity (list_max l'). +Qed. + +Section Permutation_transp. + +Variable A:Type. + +(** Permutation definition based on transpositions for induction with fixed length *) +Inductive Permutation_transp : list A -> list A -> Prop := +| perm_t_refl : forall l, Permutation_transp l l +| perm_t_swap : forall x y l1 l2, Permutation_transp (l1 ++ y :: x :: l2) (l1 ++ x :: y :: l2) +| perm_t_trans l l' l'' : + Permutation_transp l l' -> Permutation_transp l' l'' -> Permutation_transp l l''. + +Instance Permutation_transp_sym : Symmetric Permutation_transp. +Proof. + intros l1 l2 HP; induction HP; subst; try (now constructor). + now apply (perm_t_trans IHHP2). +Qed. + +Instance Permutation_transp_equiv : Equivalence Permutation_transp. +Proof. + split. + - intros l; apply perm_t_refl. + - apply Permutation_transp_sym. + - intros l1 l2 l3 ;apply perm_t_trans. +Qed. + +Lemma Permutation_transp_cons : forall (x : A) l1 l2, + Permutation_transp l1 l2 -> Permutation_transp (x :: l1) (x :: l2). +Proof. + intros x l1 l2 HP. + induction HP. + - reflexivity. + - rewrite 2 app_comm_cons. + apply perm_t_swap. + - now transitivity (x :: l'). +Qed. + +Lemma Permutation_Permutation_transp : forall l1 l2 : list A, + Permutation l1 l2 <-> Permutation_transp l1 l2. +Proof. + intros l1 l2; split; intros HP; induction HP; intuition. + - now apply Permutation_transp_cons. + - rewrite <- (app_nil_l (y :: _)). + rewrite <- (app_nil_l (x :: y :: _)). + apply perm_t_swap. + - now transitivity l'. + - apply Permutation_app_head. + apply perm_swap. + - now transitivity l'. +Qed. + +Lemma Permutation_ind_transp : forall P : list A -> list A -> Prop, + (forall l, P l l) -> + (forall x y l1 l2, P (l1 ++ y :: x :: l2) (l1 ++ x :: y :: l2)) -> + (forall l l' l'', + Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') -> + forall l1 l2, Permutation l1 l2 -> P l1 l2. +Proof. + intros P Hr Ht Htr l1 l2 HP; apply Permutation_Permutation_transp in HP. + revert Hr Ht Htr; induction HP; intros Hr Ht Htr; auto. + apply (Htr _ l'); intuition; now apply Permutation_Permutation_transp. +Qed. + +End Permutation_transp. + (* begin hide *) Notation Permutation_app_swap := Permutation_app_comm (only parsing). (* end hide *) diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 210ac754a1..0f25bc8e12 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -116,6 +116,11 @@ let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false let end_show () = restore_state () + let begin_details s = + save_state (); Cdglobals.gallina := false; Cdglobals.light := false; + Output.start_details s + let end_details () = Output.stop_details (); restore_state () + (* Reset the globals *) let reset () = @@ -434,6 +439,8 @@ let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl +let begin_details = "(*" space* "begin" space+ "details" space* +let end_details = "(*" space* "end" space+ "details" space* "*)" space* nl (* let begin_verb = "(*" space* "begin" space+ "verb" space* "*)" let end_verb = "(*" space* "end" space+ "verb" space* "*)" @@ -460,6 +467,11 @@ rule coq_bol = parse { begin_show (); coq_bol lexbuf } | space* end_show { end_show (); coq_bol lexbuf } + | space* begin_details + { let s = details_body lexbuf in + Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf } + | space* end_details + { Output.end_coq (); end_details (); Output.start_coq (); coq_bol lexbuf } | space* (("Local"|"Global") space+)? gallina_kw_to_hide { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then @@ -1221,6 +1233,19 @@ and printing_token_body = parse | _ { Buffer.add_string token_buffer (lexeme lexbuf); printing_token_body lexbuf } +and details_body = parse + | "*)" space* nl? | eof + { None } + | ":" space* { details_body_rec lexbuf } + +and details_body_rec = parse + | "*)" space* nl? | eof + { let s = Buffer.contents token_buffer in + Buffer.clear token_buffer; + Some s } + | _ { Buffer.add_string token_buffer (lexeme lexbuf); + details_body_rec lexbuf } + (*s These handle inference rules, parsing the body segments of things enclosed in [[[ ]]] brackets *) and inf_rules indents = parse diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 862715753d..dd1b65d294 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -469,6 +469,11 @@ module Latex = struct let stop_emph () = printf "}" + let start_details _ = () + + let stop_details () = () + + let start_comment () = printf "\\begin{coqdoccomment}\n" let end_comment () = printf "\\end{coqdoccomment}\n" @@ -740,6 +745,12 @@ module Html = struct let stop_emph () = printf "</i>" + let start_details = function + | Some s -> printf "<details><summary>%s</summary>" s + | _ -> printf "<details>" + + let stop_details () = printf "</details>" + let start_comment () = printf "<span class=\"comment\">(*" let end_comment () = printf "*)</span>" @@ -1053,6 +1064,9 @@ module TeXmacs = struct let start_emph () = printf "<with|font shape|italic|" let stop_emph () = printf ">" + let start_details _ = () + let stop_details () = () + let start_comment () = () let end_comment () = () @@ -1159,6 +1173,9 @@ module Raw = struct let start_emph () = printf "_" let stop_emph () = printf "_" + let start_details _ = () + let stop_details () = () + let start_comment () = printf "(*" let end_comment () = printf "*)" @@ -1272,6 +1289,11 @@ let start_emph = let stop_emph = select Latex.stop_emph Html.stop_emph TeXmacs.stop_emph Raw.stop_emph +let start_details = + select Latex.start_details Html.start_details TeXmacs.start_details Raw.start_details +let stop_details = + select Latex.stop_details Html.stop_details TeXmacs.stop_details Raw.stop_details + let start_latex_math = select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math let stop_latex_math = diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 485183a4ed..b7a8d4d858 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -29,6 +29,9 @@ val start_module : unit -> unit val start_doc : unit -> unit val end_doc : unit -> unit +val start_details : string option -> unit +val stop_details : unit -> unit + val start_emph : unit -> unit val stop_emph : unit -> unit |