coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Type casting of a dependent type

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Type casting of a dependent type
Date: Mon, 28 Sep 2020 10:37:26 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:I63+oRI3n9Rg4KHz+NmcpTZWNBhigK39O0sv0rFitYgeLPrxwZ3uMQTl6Ol3ixeRBMOHsq0C0bSd7v6ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalsIBi3ognctsgbipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPl8J+kqxbrhKiqRJxzYHbb4OaO+Zlc6zHYd8XX3BMUtpfWiFDBI63cosBD/AGPeZdt4Twu0YBogG7BQKxGu7vyjtIhn7u3aIg1+QuCxzN0Qs6EN0TqnvUqcn6ObwOXuCu1qbIzDHDY+lT2Tf89IjEaA4uruyRXb9pd8fa1EYgGR/fgFqKtYzlIy2a1v4Ls2WD7uduW/6ih3MppgxyoDWix8UhhpTXi44L11zK+yp0zJo1KNO4SUN2Yt6pHptNuiybK4d4Td0vT3x0tSsm17EIuZi2dzUExpQgwh7Qcf2Hc46Q7x3/VOaRJTZ4hGp/d7K7nRm+606gxfPgVsSyzV1ErTJFn8HRunwT1BHf8MaKRudn8ku/wzqDyR3f5v1cLUwqiabWK4QtzqAsmpYOq0jPAyv7lF/4gaOIcEgv5/Km5P79Yrr8o5+RL490hR/6MqQpgsG/Bvk4MhQBX2ic+OS80rLj8VTiQLVWlPI2jrPWvIrGKsQAvKG5AgtV3pwm6xa+EzeqysoXkmQaLF5deRKHiZbmO03WLfzlE/uygE6gnTl3y/zcILHtGIvBImXfnLv5eLZy8U9cyA49zdBF4JJUD6kML+juVUDrsdzXEgQ0PBCvw+n9CdV90pkSWWeOAq+FKq/dr0KH5v83L+mWeIAVoCr9K+Qi5/P2kXA5nkYdcbC10psTdXC3Be9rI16ZYHrpmtcOC30Gvgs4TOzwiV2NSyRfZ3ioX/F02jZuA4W/SIzHW4qFgbqb3S79EIcFSHpBDwWlHX7tP66EX/YUYSabaptonjUBXpCqUIYg0VertRO8xrZ6eLmHshYEvI7ugYAmr9bYkgs/oGQtUpatllqVRmQxpVsmAj872Kck+R5610uM1ql+jLlDCdVP7rVCSQ47MdjZzvA8BtzvCFqYIoW5DW2+S9DjOgkfC8oryoZTMU1mEtSmyBXCw2ynD6JHz+XaVqxxybrV2j3KH+g4zn/H0Kc7iFx/H5lELmSnguh69hSVCoLUwRyU

You are headed into complex territory here, and I recommend reading a comprehensive introduction, rather than proceeding one question at a time. I'm biased, but my suggestion is Chapter 10 of CPDT.

On 9/28/20 10:34 AM, 劉弘毅 wrote:

Could I ask you another question? Now, is there a way to show the equivalence of "omega" and "cast"?

I would like to do something like

omega a = cast a

Since (T (f a)) and (T (g a)) are the different expressions of the same type, these values should be comparable. However, the equation does not type-check.

Moreover, I cannot unfold the "cast" function since it is defined with "Proof" and made opaque. Is it impossible to make this kind of comparison?

[Coq-Club] Type casting of a dependent type, 劉弘毅, 09/28/2020
- Re: [Coq-Club] Type casting of a dependent type, Maximilian Wuttke, 09/28/2020
  - Re: [Coq-Club] Type casting of a dependent type, 劉弘毅, 09/28/2020
    - Re: [Coq-Club] Type casting of a dependent type, Adam Chlipala, 09/28/2020
      - Re: [Coq-Club] Type casting of a dependent type, 劉弘毅, 09/28/2020
        
        Re: [Coq-Club] Type casting of a dependent type, 劉弘毅, 09/28/2020
    - Re: [Coq-Club] Type casting of a dependent type, Maximilian Wuttke, 09/28/2020