naive_simpl.v 11.6 KB
Newer Older
 Michael Sammler committed Jul 21, 2020 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 ``````From refinedc.typing Require Import typing. Set Default Proof Using "Type". Lemma tac_eq_replace (P1 P2 : Prop): P2 = P1 → P1 → P2. Proof. by move => ->. Qed. Lemma tac_f_equal_fn {A B} (f1 f2 : A → B) x1 x2 r: x1 = x2 → f1 = f2 → f2 x2 = r → f1 x1 = r. Proof. by move => -> -> ->. Qed. Lemma tac_f_equal_fn2 {A B} (f1 f2 : A → B) x1 x2 r: x1 = x2 → f1 = f2 → f2 x2 = r → r = r → f1 x1 = r. Proof. by move => -> -> ->. Qed. (* Lemma tac_apply_Normalize {A B} (f1 f2 : A → B) x1 x2 r: *) (* x1 = x2 → f1 = f2 → f1 x1 = r. *) (* Proof. by move => -> -> ->. Qed. *) Goal ∀ l i (x : Z), -1 < length (<[i:=x]> \$ <[i:=x]> (<[length (<[i:=x]>l) :=x]> l ++ <[length (<[i:=x]>l) :=x]> l)). move => ???. (* Time normalize_goal. *) (* Time notypeclasses refine (tac_normalize_goal _ _ _ _); [normalize_autorewrite|]. *) lia. Abort. Ltac normalize2 P cont := let typeP := type of P in let do_nothing x := (* idtac "do nothing " P; *) cont P uconstr:(@eq_refl typeP P) in (* idtac "starting" P; *) lazymatch P with | ?f ?a => lazymatch type of f with | ?A → ?B => normalize2 a ltac:(fun a' Heqa => normalize2 f ltac:(fun f' Heqf => let r := fresh "r" in let Hr := fresh "Hr" in first [ simple notypeclasses refine (let r := _ in let Hr := _ : Normalize (f' a') r in _); [shelve| unfold r; solve [refine _ ] |]; (* simple notypeclasses refine (let r := _ in (λ Hr : Normalize (f' a') r, _) _); [shelve| | unfold r; solve [refine _ ]]; *) let r' := eval unfold r in r in (* let Hr' := eval unfold Hr in Hr in *) unfold r,Normalize in Hr; (* clear r Hr; *) clear r; (* idtac f a "-" r'; *) assert_fails (constr_eq_strict constr:(f a) r'); (* idtac "found!" r'; *) (* let Hrt := type of Hr in idtac "Hr" Hr Hrt; *) (* let c:= constr:(normalize (Normalize := Hr)) in let ct := type of c in idtac c ct; *) cont r' uconstr:(@tac_f_equal_fn A B f f' a a' r' Heqa Heqf Hr); clear Hr (* idtac "constr2" r' *) | do_nothing O ])) (* idtac "nothong..."; *) (* do_nothing () *) (* idtac "after do nothing1" P *) (* else ( *) (* idtac "found!" r'; *) (* idtac "cont!" P; *) (* idtac "found2!" r'; *) (* idtac "cont2!" P; *) (* idtac "after cont" P *) (* ))) *) | _ => do_nothing O end | _ => do_nothing O end. Ltac normalize3 := lazymatch goal with | |- @eq ?A ?P _ => lazymatch P with | ?f ?a => lazymatch type of f with | ?A → ?B => ( notypeclasses refine (tac_f_equal_fn _ _ _ _ _ _ _ _); [normalize3|normalize3| lazymatch goal with `````` Michael Sammler committed Sep 03, 2020 89 `````` | |- ?A = ?B => change_no_check (Normalize A B) `````` Michael Sammler committed Jul 21, 2020 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 `````` end; solve [ refine _ ] ]) || exact: eq_refl | _ => exact: eq_refl end | _ => exact: eq_refl end end. Ltac normalize_goal2 := match goal with | |- ?P => normalize2 P ltac:(fun P' Heq => notypeclasses refine (tac_eq_replace P' P Heq _) ) end. Ltac normalize_goal3 := match goal with | |- ?P => notypeclasses refine (tac_eq_replace _ _ _ _); [normalize3|] end. Ltac normalize4 := lazymatch goal with | |- @eq ?A ?P ?B => let rec go ctx P := lazymatch P with | ?f ?a => lazymatch type of f with | ?A → ?B => ( (* idtac ctx P f a; *) let fctx := eval lazy beta in (λ x, ctx (x a)) in go fctx f; let actx := eval lazy beta in (λ x, ctx (f x)) in go actx a; refine (eq_ind_r ctx _ _);[| lazymatch goal with `````` Michael Sammler committed Sep 03, 2020 127 `````` | |- ?A = ?B => change_no_check (Normalize A B) `````` Michael Sammler committed Jul 21, 2020 128 129 130 131 132 133 134 135 `````` end; solve [ refine _ ] ] ) || idtac (* ( *) (* notypeclasses refine (tac_f_equal_fn _ _ _ _ _ _ _ _); *) (* [normalize3|normalize3| *) (* lazymatch goal with *) `````` Michael Sammler committed Sep 03, 2020 136 `````` (* | |- ?A = ?B => change_no_check (Normalize A B) *) `````` Michael Sammler committed Jul 21, 2020 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 `````` (* end; solve [ refine _ ] ]) || *) (* exact: eq_refl *) | _ => idtac (* idtac "end" P *) (* exact: eq_refl *) end | _ => idtac (* idtac "end" P *) (* exact: eq_refl *) end in go constr:(λ x: A, x = B) P; exact: eq_refl (* end in *) (* go ltac:(fun i => uconstr:(λ x, i x = B)) P; exact: eq_refl *) end. Ltac normalize_goal4 := match goal with | |- ?P => notypeclasses refine (tac_eq_replace _ _ _ _); [normalize4|] end. (* Goal True. *) (* simple notypeclasses refine (let x := _ in let H := _ : Normalize 0 x in _); [shelve| unfold x; solve [refine _ ] |]. *) (* (* Set Printing All. *) *) (* let Hr := eval unfold H in H in idtac Hr. *) (* notypeclasses refine ( (λ x : Z, λ H : Normalize 0 x, _ ) _ _). *) `````` Michael Sammler committed Oct 19, 2021 163 ``````#[export] Hint Rewrite @insert_length @app_length : test_db. `````` Michael Sammler committed Jul 21, 2020 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 ``````Goal ∀ l i (x : Z), 0%nat = length (<[i:=x]> l). intros. (* let ctx := ltac:(fun i => uconstr:(λ x, ltac:(i x) = 0)) in *) (* let ctx' := ctx ltac:(fun x => idtac x; x) in idtac ctx'. *) (* Set Typeclasses Debug Verbosity 2. *) (* normalize_goal. *) normalize_goal4. (* unshelve let a := uconstr:(fun xxx => uconstr:(xxx)) in idtac a. *) (* Show Proof. *) (* Time normalize_goal. *) (* Time autorewrite with test_db. *) (* Show Proof. *) notypeclasses refine (tac_eq_replace _ _ _ _). 2: shelve. (* notypeclasses refine (tac_f_equal_fn _ _ _ _ _ _ _ _); *) (* [normalize3|normalize3| *) (* lazymatch goal with *) `````` Michael Sammler committed Sep 03, 2020 186 `````` (* | |- ?A = ?B => change_no_check (Normalize true A B) *) `````` Michael Sammler committed Jul 21, 2020 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 `````` (* end; solve [ refine _ ] ]. *) (* progress (refine (tac_f_equal_fn _ _ _ _ _ _ _ _);[ exact: eq_refl..|]). *) Abort. (* move => l i x. *) (* (* (* notypeclasses refine (tac_eq_replace (0 = length l) (0 = length (<[i:=x]> l)) _ _). *) *) *) (* (* (* ((0 = strings.length (<[i:=x]> l)) = (0 = strings.length l)) *) *) *) (* (* (* Set Ltac Debug. *) *) *) (* normalize_goal2. *) (* tryif idtac then idtac "a"; idtac "b" else idtac "b"; idtac "d". *) Goal ∀ l i (x : Z), -1 < length (<[i:=x]> \$ <[i:=x]> (<[length (<[i:=x]>l) :=x]> l ++ <[length (<[length (<[length (<[i:=x]>l):=x]>l):=x]>l) :=x]> l)). move => ???. (* Time normalize_goal. *) (* Time notypeclasses refine (tac_normalize_goal _ _ _ _); [normalize_autorewrite|]. *) (* Show Proof. *) (* Time autorewrite with test_db. *) (* Show Proof. *) (* Show Proof. *) (* Time normalize_goal4. *) (* Show Proof. *) (* Time rewrite_strat (topdown (choice insert_length app_length)). *) (* nmo *) (* normalize_goal3. *) (* notypeclasses refine (tac_eq_replace _ _ _ _). 2: shelve. *) (* ( *) (* notypeclasses refine (tac_f_equal_fn _ _ _ _ _ _ _ _); *) (* [normalize3|normalize3| *) (* lazymatch goal with *) `````` Michael Sammler committed Sep 03, 2020 222 `````` (* | |- ?A = ?B => change_no_check (Normalize A B) *) `````` Michael Sammler committed Jul 21, 2020 223 224 225 226 227 228 229 `````` (* end; solve [ refine _ ] ]). *) (* exact: eq_refl. *) (* normalize3. *) (* notypeclasses refine (tac_f_equal_fn2 _ _ _ _ _ _ _ _ _); *) (* [normalize3|normalize3| *) (* lazymatch goal with *) `````` Michael Sammler committed Sep 03, 2020 230 `````` (* | |- ?A = ?B => change_no_check (Normalize A B) *) `````` Michael Sammler committed Jul 21, 2020 231 232 233 234 235 236 237 `````` (* end; solve [ refine _ ] | ]. *) (* notypeclasses refine (tac_eq_replace _ _ _ _). *) (* notypeclasses refine (tac_f_equal_fn _ _ _ _ _ _ _ _). exact: eq_refl. exact: eq_refl. *) (* lazymatch goal with *) `````` Michael Sammler committed Sep 03, 2020 238 `````` (* | |- ?A = ?B => change_no_check (Normalize A B) *) `````` Michael Sammler committed Jul 21, 2020 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 `````` (* end. *) (* (* let x := (1 + 1) in idtac x. *) *) (* (* simple notypeclasses refine (let r := _ in (λ Hr : Normalize (0) r, _) _). *) *) (* normalize_goal2. *) (* Set Printing Implicit. Show Proof. (* normalize_goal2. *) *) lia. Qed. Goal ∀ l i (x : Z), seq 0%nat 50%nat ++ [length (<[length (<[i:=x]> l):=x]> l)] ≠ []. intros. simpl. (* Time autorewrite with test_db. *) (* Time notypeclasses refine (tac_normalize_goal _ _ _ _); [normalize_autorewrite|]. *) (* Set Typeclasses Debug. *) (* Time normalize_goal. *) (* Show Proof. *) (* Time normalize_goal2. *) (* Time normalize_goal3. *) (* Time normalize_goal4. *) (* done. *) (* Show Proof. *) (* Time Qed. *) Abort. (* { simpl. Time normalize_goal2. Set Printing Implicit. Show Proof. Time normalize_goal2. admit. } *) Goal True. (* assert True as G. Show Proof. admit. *) (* have : ∃ a : nat, a = a. eexists _. Show Proof. *) (* notypeclasses refine ((λ a, (λ H : Normalize O a , _ ) _) _). admit. revert H. Show Proof. *) (* assert (∃ P, Normalize n *) (* constr_eq_strict constr:(S O) (S O). *) (* evar (r : (list nat → Prop)). *) (* assert (Normalize (eq (@nil nat)) r) as Hr. unfold r. *) (* apply normalize_end. *) (* ; [solve [refine _] |]. *) (* have : seq 0%nat 0%nat = []. { simpl. Time normalize_goal. Time normalize_goal2. admit. } *) (* have : seq 0%nat 10%nat = []. { simpl. Time normalize_goal. Time normalize_goal2. admit. } *) (* have : seq 0%nat 50%nat = []. { simpl. Time normalize_goal. Time normalize_goal2. admit. } *) (* have : seq 0%nat 100%nat = []. { simpl. Time normalize_goal. Time normalize_goal2. admit. } *) Abort. Definition shelve_marker (P : Prop) : Prop := P. Ltac naive_simpl_go := lazymatch goal with | |- _ → _ => lazymatch goal with (* relying on the fact that unification variables cannot contain dependent variables to distinguish between dependent and non dependent forall *) | |- ?P -> ?Q => lazymatch type of P with | Prop => first [ progress normalize_goal_impl | notypeclasses refine (apply_simpl_impl _ _ _ _ _); [ solve [refine _] |]; simpl; match goal with | |- true = true -> _ => move => _ | |- false = false -> ?P → _ => move => _; match P with | ∃ _, _ => case | _ = _ => let Hi := fresh "Hi" in move => Hi; injection Hi; clear Hi `````` Michael Sammler committed Nov 19, 2021 305 `````` | _ => assert_is_not_trivial P; intros ?; subst `````` Michael Sammler committed Jul 21, 2020 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 `````` | _ => move => _ end end] (* just some unused variable, forget it *) | _ => move => _ end | |- forall _ : ?P, _ => lazymatch P with | (prod _ _) => case | unit => case | _ => intro end end | |- _ ∧ _ => first [ progress normalize_goal_and | notypeclasses refine (apply_simpl_and _ _ _ _ _); [ solve [refine _] |]; simpl; lazymatch goal with | |- true = true -> _ => move => _ | |- false = false -> ?P ∧ _ => move => _; match P with (* TODO: Is this a good idea? *) | _ → _ => split | protected ?H = ?x => liInst H x | ?x = protected ?H => liInst H x | _ => split; [fast_done || change (shelve_marker P); shelve | ] end end ] | |- @ex ?A ?P => first [ lazymatch A with (* | prod _ _ => apply: tac_exist_prod *) (* | sigT _ => apply: tac_exist_sigT *) | unit => exists tt (* | ?A => let Hevar := create_protected_evar A in exists (protected Hevar) *) end | change (shelve_marker (@ex A P)); shelve ] | |- True => exact: I | _ => refine (intro_and_True _ _) end. Ltac naive_simpl := unshelve (repeat naive_simpl_go); match goal with | |- shelve_marker ?P => change P; first [ progress unfold_instantiated_evars; naive_simpl | idtac ] | _ => shelve end. Ltac naive_solve := naive_simpl; solve_goal. Ltac can_solve_tac ::= naive_solve.``````