@@ -4,11 +4,12 @@ From MetaCoq.Quotation.ToTemplate Require Import Init.
44From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Numbers Coq.Init Coq.Lists.
55From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig.
66From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.FSets Require Import FMapInterface.Sig FMapFacts.Sig FMapAVL.Sig FMapList.Sig.
7+ From MetaCoq.Quotation.ToTemplate.QuotationOf.Utils Require Import MCFSets.Sig.
78
89#[export] Hint Unfold Int.Z_as_Int.t : quotation.
910
10- Module QuoteWSfun (E : DecidableTypeOrig) (Import W : WSfun E) (Import WFacts : WFacts_funSig E W) (qE : QuotationOfDecidableTypeOrig E) (qW : QuotationOfWSfun E W) (qWFacts : QuotationOfWFacts_fun E W WFacts).
11- Import (hints) qE qW qWFacts.
11+ Module QuoteWSfun (E : DecidableTypeOrig) (Import W : WSfun E) (Import WFacts : WFacts_funSig E W) (Import WFactsExtra : WFactsExtra_funSig E W WFacts) ( qE : QuotationOfDecidableTypeOrig E) (qW : QuotationOfWSfun E W) (qWFacts : QuotationOfWFacts_fun E W WFacts) (qWFactsExtra : QuotationOfWFactsExtra_fun E W WFacts WFactsExtra ).
12+ Import (hints) qE qW qWFacts qWFactsExtra .
1213 #[export] Hint Unfold Int.Z_as_Int.t : quotation.
1314
1415 Section with_quote.
@@ -27,62 +28,14 @@ Module QuoteWSfun (E : DecidableTypeOrig) (Import W : WSfun E) (Import WFacts :
2728 #[export] Instance quote_neg_Empty {m} {qm : quotation_of m} : ground_quotable (~@Empty elt m)
2829 := quote_neg_of_iff (iff_sym (@is_empty_iff _ _)).
2930
30- Definition Equiv_alt (eq_elt : elt -> elt -> Prop ) m m' :=
31- let eq_opt_elt x y := match x, y with
32- | Some x, Some y => eq_elt x y
33- | None, None => True
34- | Some _, None | None, Some _ => False
35- end in
36- List.Forall (fun '(k, _) => eq_opt_elt (find k m) (find k m')) (@elements elt m)
37- /\ List.Forall (fun '(k, _) => eq_opt_elt (find k m) (find k m')) (@elements elt m').
3831 Import StrongerInstances.
39- Lemma Equiv_alt_iff {eq_elt m m'} : Equiv_alt eq_elt m m' <-> Equiv eq_elt m m'.
40- Proof using Type .
41- cbv [Equiv Equiv_alt].
42- cbv [In] in *.
43- setoid_rewrite find_mapsto_iff.
44- rewrite !Forall_forall.
45- pose proof (@find_o elt m).
46- pose proof (@find_o elt m').
47- transitivity
48- (let eq_opt_elt x y := match x, y with
49- | Some x, Some y => eq_elt x y
50- | None, None => True
51- | Some _, None | None, Some _ => False
52- end in
53- (forall k, In k m -> eq_opt_elt (find k m) (find k m'))
54- /\ (forall k, In k m' -> eq_opt_elt (find k m) (find k m'))).
55- 1: cbv [In]; setoid_rewrite elements_mapsto_iff; setoid_rewrite InA_alt; cbv [eq_key_elt]; cbn [fst snd].
56- 2: cbv [In]; setoid_rewrite find_mapsto_iff.
57- all: repeat (split || intros || destruct_head'_and || split_iff || destruct_head'_prod || destruct_head'_ex || subst).
58- all: specialize_dep_under_binders_by eapply ex_intro.
59- all: specialize_dep_under_binders_by eapply conj.
60- all: specialize_dep_under_binders_by eapply eq_refl.
61- all: specialize_dep_under_binders_by eapply pair.
62- all: cbn [fst snd] in *.
63- all: specialize_all_ways_under_binders_by apply E.eq_refl.
64- all: repeat first [ progress destruct_head'_ex
65- | match goal with
66- | [ H : List.In _ _ |- _ ]
67- => progress specialize_under_binders_by exact H
68- | [ H : E.eq _ _ |- _ ]
69- => progress specialize_under_binders_by exact H
70- | [ H : find _ _ = Some _ |- _ ]
71- => progress specialize_under_binders_by exact H
72- end ].
73- all: try solve [ repeat destruct ?; subst; try congruence; eauto ].
74- Qed .
32+ #[export] Instance quote_Equiv_alt {eq_elt} {m m'} {qeq_elt : quotation_of eq_elt} {quote_elt : ground_quotable elt} {quote_key : ground_quotable key} {quote_eq_elt : forall x y, ground_quotable (eq_elt x y:Prop)} {qm : quotation_of m} {qm' : quotation_of m'} : ground_quotable (@Equiv_alt elt eq_elt m m') := ltac:(cbv [Equiv_alt]; exact _).
7533
76- #[export] Instance quote_Equiv_alt {eq_elt} {m m'} {qeq_elt : quotation_of eq_elt} {quote_elt : ground_quotable elt} {quote_key : ground_quotable key} {quote_eq_elt : forall x y, ground_quotable (eq_elt x y:Prop)} {qm : quotation_of m} {qm' : quotation_of m'} : ground_quotable (@Equiv_alt eq_elt m m') := ltac:(cbv [Equiv_alt]; exact _).
77- #[local] Instance qEquiv_alt : quotation_of (@Equiv_alt) := ltac:(unfold_quotation_of (); exact _).
78- (* too slow :-( *)
79- (*#[local] Instance qEquiv_alt_iff : quotation_of (@Equiv_alt_iff) := ltac:(unfold_quotation_of (); exact _). *)
34+ #[export] Instance quote_Equiv {eq_elt m m'} {qm : quotation_of m} {qm' : quotation_of m'} {quote_elt : ground_quotable elt} {quote_key : ground_quotable key} {qeq_elt : quotation_of eq_elt} {quote_eq_elt : forall x y, ground_quotable (eq_elt x y:Prop)} : ground_quotable (@Equiv elt eq_elt m m') := ground_quotable_of_iff Equiv_alt_iff.
8035
81- #[export] Instance quote_Equiv {qEquiv_alt_iff : quotation_of (@Equiv_alt_iff)} {qEquiv_alt_iff : quotation_of (@Equiv_alt_iff)} {eq_elt m m'} {qm : quotation_of m} {qm' : quotation_of m'} {quote_elt : ground_quotable elt} {quote_key : ground_quotable key} {qeq_elt : quotation_of eq_elt} {quote_eq_elt : forall x y, ground_quotable (eq_elt x y:Prop)} : ground_quotable (@Equiv elt eq_elt m m') := ground_quotable_of_iff Equiv_alt_iff .
36+ #[export] Instance quote_Equal { m m'} {qm : quotation_of m} {qm' : quotation_of m'} {quote_elt : ground_quotable elt} {quote_key : ground_quotable key} : ground_quotable (@Equal elt m m') := ground_quotable_of_iff (iff_sym (@Equal_Equiv elt m m')) .
8237
83- #[export] Instance quote_Equal {qEquiv_alt_iff : quotation_of (@Equiv_alt_iff)} {m m'} {qm : quotation_of m} {qm' : quotation_of m'} {quote_elt : ground_quotable elt} {quote_key : ground_quotable key} : ground_quotable (@Equal elt m m') := ground_quotable_of_iff (iff_sym (@Equal_Equiv elt m m')).
84-
85- #[export] Instance quote_Equivb {qEquiv_alt_iff : quotation_of (@Equiv_alt_iff)} {cmp m m'} {qm : quotation_of m} {qm' : quotation_of m'} {quote_elt : ground_quotable elt} {quote_key : ground_quotable key} {qcmp : quotation_of cmp} : ground_quotable (@Equivb elt cmp m m') := ltac:(cbv [Equivb Cmp]; exact _).
38+ #[export] Instance quote_Equivb {cmp m m'} {qm : quotation_of m} {qm' : quotation_of m'} {quote_elt : ground_quotable elt} {quote_key : ground_quotable key} {qcmp : quotation_of cmp} : ground_quotable (@Equivb elt cmp m m') := ltac:(cbv [Equivb Cmp]; exact _).
8639 End with_quote.
8740
8841 #[export] Existing Instances
@@ -106,94 +59,24 @@ Module QuoteWSfun (E : DecidableTypeOrig) (Import W : WSfun E) (Import WFacts :
10659 .
10760End QuoteWSfun.
10861
109- Module QuoteFMapAVL (T : OrderedTypeOrig) (M : FMapAVL.MakeSig T) (Import WFacts : WFacts_funSig T M) (qT : QuotationOfOrderedTypeOrig T) (qM : FMapAVL.QuotationOfMake T M) (qWFacts : QuotationOfWFacts_fun T M WFacts).
110- Import (hints) qT qM qWFacts.
111- Include QuoteWSfun T M WFacts qT qM qWFacts.
62+ Module QuoteFMapAVL (T : OrderedTypeOrig) (M : FMapAVL.MakeSig T) (Import WFacts : WFacts_funSig T M) (Import WFactsExtra : WFactsExtra_funSig T M WFacts) (Import MDecide : FMapAVL.DecideSig T M) ( qT : QuotationOfOrderedTypeOrig T) (qM : FMapAVL.QuotationOfMake T M) (qWFacts : QuotationOfWFacts_fun T M WFacts) (qWFactsExtra : QuotationOfWFactsExtra_fun T M WFacts WFactsExtra) (qMDecide : FMapAVL.QuotationOfDecide T M MDecide ).
63+ Import (hints) qT qM qWFacts qWFactsExtra qMDecide .
64+ Include QuoteWSfun T M WFacts WFactsExtra qT qM qWFacts qWFactsExtra .
11265
11366 Module Raw.
114- Scheme Induction for M.Raw.tree Sort Type .
115- Scheme Induction for M.Raw.tree Sort Set .
116- Scheme Induction for M.Raw.tree Sort Prop .
117- Scheme Case for M.Raw.tree Sort Type .
118- Scheme Case for M.Raw.tree Sort Prop .
119- Scheme Minimality for M.Raw.tree Sort Type .
120- Scheme Minimality for M.Raw.tree Sort Set .
121- Scheme Minimality for M.Raw.tree Sort Prop .
122-
12367 Section with_t.
12468 Context {elt : Type }
12569 {qelt : quotation_of elt}
12670 {quote_elt : ground_quotable elt} {quote_T_t : ground_quotable T.t}.
12771
128- Fixpoint lt_tree_dec x t : { @M.Raw.lt_tree elt x t } + {~ @M.Raw.lt_tree elt x t}.
129- Proof .
130- refine match t with
131- | M.Raw.Leaf => left _
132- | M.Raw.Node l k n r z
133- => match T.compare k x, lt_tree_dec x l, lt_tree_dec x r with
134- | LT p1, left p2, left p3 => left _
135- | _, right pf, _ => right _
136- | _, _, right pf => right _
137- | _, _, _ => right _
138- end
139- end;
140- try solve [ inversion 1
141- | inversion 1; subst; auto;
142- match goal with
143- | [ H : T.lt _ _, H' : T.eq _ _ |- _ ]
144- => now first [ rewrite -> H' in H | rewrite <- H' in H ]
145- end
146- | intro f; apply pf; hnf in *; intros; apply f; constructor; (assumption + reflexivity)
147- | intro f; eapply M.Raw.Proofs.MX.lt_antirefl; (idtac + etransitivity); (eassumption + (eapply f; constructor; (idtac + symmetry); (eassumption + reflexivity))) ].
148- Defined .
149- Fixpoint gt_tree_dec x t : { @M.Raw.gt_tree elt x t } + {~ @M.Raw.gt_tree elt x t}.
150- Proof .
151- refine match t with
152- | M.Raw.Leaf => left _
153- | M.Raw.Node l k n r z
154- => match T.compare k x, gt_tree_dec x l, gt_tree_dec x r with
155- | GT p1, left p2, left p3 => left _
156- | _, right pf, _ => right _
157- | _, _, right pf => right _
158- | _, _, _ => right _
159- end
160- end;
161- try solve [ inversion 1
162- | inversion 1; subst; auto;
163- match goal with
164- | [ H : T.lt _ _, H' : T.eq _ _ |- _ ]
165- => now first [ rewrite -> H' in H | rewrite <- H' in H ]
166- end
167- | intro f; apply pf; hnf in *; intros; apply f; constructor; (assumption + reflexivity)
168- | intro f; eapply M.Raw.Proofs.MX.lt_antirefl; (idtac + etransitivity); (eassumption + (eapply f; constructor; (idtac + symmetry); (eassumption + reflexivity))) ].
169- Defined .
170- Fixpoint bst_dec t : { @M.Raw.bst elt t } + {~ @M.Raw.bst elt t}.
171- Proof .
172- refine match t with
173- | M.Raw.Leaf => left _
174- | M.Raw.Node l k n r z
175- => match bst_dec l, bst_dec r, lt_tree_dec k l, gt_tree_dec k r with
176- | right pf, _, _, _ => right _
177- | _, right pf, _, _ => right _
178- | _, _, right pf, _ => right _
179- | _, _, _, right pf => right _
180- | left p1, left p2, left p3, left p4 => left _
181- end
182- end;
183- try solve [ constructor; assumption
184- | inversion 1; subst; auto ].
185- Defined .
18672 #[local] Hint Unfold M.Raw.key : quotation.
18773 #[export] Instance quote_tree : ground_quotable (M.Raw.tree elt) := (ltac:(induction 1; exact _)).
188- (* very slow :-( *)
189- #[local] Instance qlt_tree_dec : quotation_of (@lt_tree_dec) := ltac:(unfold_quotation_of (); exact _).
190- #[local] Instance qgt_tree_dec : quotation_of (@gt_tree_dec) := ltac:(unfold_quotation_of (); exact _).
191- #[local] Instance qbst_dec : quotation_of (@bst_dec) := ltac:(unfold_quotation_of (); exact _).
19274 #[export] Instance quote_bst t : ground_quotable (M.Raw.bst t)
193- := ground_quotable_of_dec (@bst_dec t).
75+ := ground_quotable_of_dec (@Raw. bst_dec elt t).
19476 End with_t.
19577 #[export] Hint Unfold M.Raw.key : quotation.
19678 #[export] Existing Instances
79+ quote_tree
19780 quote_bst
19881 .
19982 End Raw.
0 commit comments