coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?
Chronological Thread
- From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
- To: Jason Gross <jasongross9 AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>, Pierre Courtieu <pierre.courtieu AT gmail.com>
- Subject: Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?
- Date: Sun, 7 Feb 2021 14:14:07 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f177.google.com
- Ironport-phdr: 9a23:3BXLsx3h8nuJN0KNsmDT+DRfVm0co7zxezQtwd8ZseMQKvad9pjvdHbS+e9qxAeQG9mCurQZ0qGP6v+ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmT6wbalyIRmrogndq9QajIl/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTlkzkMOSIn/27Li8xwlKNbrwynpxxj2I7ffYWZOONjcq/BYd8WQGxMVdtTWSNcGIOxd4UBAeofM+hFrIfypVUOoxyxCgawC+3i0SNIhmbs0KEmyektDQPL0Qo9FNwOqnTUq9D1Ob8cXeC3y6nIyzTDb/BI1jf59ofHbAssof6JXb1qcMrRzVMjGB/CjlWVp4DuIjSY1uYKs2id7upgVvygi2o5pA5vuTWvycIshZPIhoIR0FzL6SJ5wIMsKNC+VUV0bsKqHoFKuCGGK4t5XNkiQ2dwtSsm1LELu5G2cTYIxZkmyRDRa+CKfoiM7x/9VeucPyp1iXJ5dL6ihhu+71atx/DiW8S7zFpHsCRLn8XPu30J1xHe7NWMRPhl/kq5xzqDywTe5vtHLE00j6bXNYAtzqAqmpYOs0nOHDf6lFv3gaOKa0kp//Wk5uD7bbjjqZKRNpN4hh37P6gzhMCyBeE1PhYBUmiV5+ux0abs8E33QLVEi/A2nLfWsJ7EKckepqO0DQxY0ogl5h2iFTmpys4YkmMCLF9deBKIkYzpO1bWLfD9F/i/glCsnC5yx/DFI7HtG5vNImXBnbrjZ7p95ElcyA08zdBb+Z1YEK0OIPX2WkPptdzYCAE2MxCszur5FNlw0pkSVGGPD6ODLq/er0GE6vgyL+SOZoIZoDP9JOIk5/7qg385g1gdfayx0JsVb3C4GPVmI0aHbnronNgOD3wHvgU7TOPwiV2CVSRfaGq1X6I5/j07Ep6pDZ/fRoCxh7yMxDu0HppPZmxfFl+MFWroeJ6fVvcXaCOSJ9dhnSYeWbigTY8hzxCuuxXgx7ppNOqHshEf4LDqz99zr8LJkgopvWh2Bt+a1W6XSHpvz0sHQjY32OZ0pkkrmXmZ1q0tyf5fE91Q6vdEXy81MJfdy6pxDNW4ElbDedGIS1uiT9iODjQ4T9Z3yNgLNRUuU+6+hwzOinL5S4QekKaGUdltqvqFgyrBYv1lwnOD75EPykE8S5IWZ2Kjj697sQPUAtyRyhjLp+ORba0ZmRX12iKDwG6J5h8KVQdxVeDcXilaaBKJ8pL24UTNS7LoArMiYFMYmJyyb5BSY9istm1oAfLqOdDQeWW0wj7iChOBx7fKZ43vKTwQ
Still not working.
#11435 comes up with "issubtype Type@{i+1} Type@{j+1}" which I want to
fail when i and j have no constraints between them. The bug causes
them to pass because "constr:(Type@{i+1}:Type@{j+1})" fails to
typecheck when it should.
But, it's close:
Ltac issubtype A B :=
first [let _:=constr:(B:A) in fail 1 B "can be ∈" A
|lazymatch constr:((fun x=>x):(A->B)) with
| fun x => x => idtac
| _ => fail 1 "A coercion exists from " A "to" B
end
|fail 1 A "and" B "are constrained to be unrelated"
].
(*Get i and j as unrelated universes:*)
Example test@{i j}(A:Type@{i})(B : Type@{j}) : True.
Proof.
Fail issubtype A B.
Fail issubtype B Type@{j}.
Fail issubtype A Type@{j}.
Fail issubtype B Type@{i}.
Fail issubtype Type@{i} Type@{j}.
Fail issubtype Type@{j} Type@{i}.
issubtype Type@{i} Type@{max(i,j)}.
issubtype Type@{i} Type@{max(i,j+1)}.
issubtype Type@{i} Type@{max(i+1,j)}.
issubtype Type@{i} Type@{i+1}.
issubtype Set Type@{Set+1}.
issubtype A A.
issubtype Prop Set.
issubtype SProp Set.
Fail issubtype Set Prop.
issubtype SProp Prop.
Fail issubtype Prop SProp.
- [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/05/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/05/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/05/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, Pierre Courtieu, 02/06/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/07/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, Jason Gross, 02/07/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/07/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, Jason Gross, 02/07/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/07/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/07/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/07/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, Jason Gross, 02/07/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/07/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, Pierre Courtieu, 02/06/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/05/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/05/2021
Archive powered by MHonArc 2.6.19+.