coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: 劉弘毅 <liukoki AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Type casting of a dependent type
Date: Tue, 29 Sep 2020 00:08:20 +0900
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=liukoki AT gmail.com; spf=Pass smtp.mailfrom=liukoki AT gmail.com; spf=None smtp.helo=postmaster AT mail-oo1-f54.google.com
Ironport-phdr: 9a23:uHYc2hPjYTsZic6mNfwl6mtUPXoX/o7sNwtQ0KIMzox0LfX7rarrMEGX3/hxlliBBdydt6sbzbCI+P66EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oMhm7rArdu8gIjYB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaksN/jKxZrxyhqRJxwJPabp+JO/dlZKzRYckXSHBdUspNVSFMBJ63YYsVD+oGOOZVt4//pV0IrxCjAgSsAOLvyiJLhn/x3q060v8sEQ7D3AM6HtIOtG7Yo8nyNKcXSO24yrTDwjrfYf1Mwzj99JTIfQ47ofGKRb98b9TcxEYsGg3KklidqZLpMy2b2OkTsGWW7/RtWOOuhmM5pQx/rSajy8YyhoTXmo8Yy0zJ+CtlzYorO9C1SkF1bNi5G5VesCGaMpF5QsIkQ2xwpCk6yrkGuZ+jfCcQzJQo3QTTa/qZfIiU5B/oSeWfIS9giX57ZL6ygwy+/Eugx+HmS8W50UtGojBFn9TDsH0Gygbd5dKdSvRn+0eswTaP2B7X6uFDOU00kLDUK58lwrIpkZoTtlnPEjb4mEj2g6KabEok+u+v6+ToZrXpuIWQOJNzigH7Kqgum8q/DvokMgUWQWSX5eCx2Kfg8ED5WrlGk/w7nrTDvJ3aKskXvqu5DBVU0oYn5Ra/FTCm0NEAkHkDLVJFZRGHj4/qO1HPO/34AvK/jE6tkDdv3fzJIrrhApDVInjZjLjhZap961JbyAcr0d9f4ItUBqgdL/L3R0/+r8fVDgQ5Mgyx2+boEs9x1oIYWWKVA6+WKrnesVGS5rFnH+7Zb4gM/T35NvIN5vj0jHZ/l0VOU7Ou2M7vkIjwSvBnPkaeYnvEjdIIEGNMtQ07Gr+5wGaeWCJeMi7hF5k34Ss2Xdr/XNXzA7u1ibnE5x+VW5hfZ2RIEFeJSC66eICNWvNKYyWXcJY4z240EIO5Qopk7imA8Q/3z709c7jR8ywc8JXkjZ17urGVmhY1+jh5Sc+a1jPVFj0mriYzXzYzmZtHjwll0F7aiPp3hvVZEZpY4PYbCgo=

Thanks. Yeah, it seems that I don't have enough understanding of the proofs regarding dependent types yet. I'm gonna get a basic understanding of the field with a textbook, and CPDT seems a good one. Thanks for introducing that to me.

On Mon, Sep 28, 2020 at 11:37 PM Adam Chlipala <adamc AT csail.mit.edu> wrote:

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