Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?

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.




Archive powered by MHonArc 2.6.19+.

Top of Page