coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Type casting of a dependent type

From: 劉弘毅 <liukoki AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Type casting of a dependent type
Date: Mon, 28 Sep 2020 15:40:35 +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-oi1-f177.google.com
Ironport-phdr: 9a23:MXFISRc0Yt2nvtai7fNgQZyXlGMj4u6mDksu8pMizoh2WeGdxcu/Zx7h7PlgxGXEQZ/co6odzbaP7Oa6BCdZuM/JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRe7oR/PusQWjoduN7s9xgbUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+uqBxxzYDXbo+IKvRxYrjQcskGSWdbRMtdSzBND4G6YoASD+QBJ+FYr4zlqlkIqxm8AxSnCeTryj9Jm3/23qo60+cgEQzd0wwgGsgBsHXQrNnvKKgSVuW1wbDOwD7eYPxYxS3z55LUchA9v/6MR7RwfNLex0QyCQ7IgFqdpIPmMj6X1ukDs2aV4u5hWO+zi2Aqth18riWzysotiYTFmpwZxk7Z+Sh6wIs4ON22RVN1bNCqFpZbqiKUN5NuT888X21lvDw2x74GtJKhYSQHyZYqywTCZ/GFcYWF5A/oWvyLLjdinn1lfaqyhxas/kikze3xTsy030xLripBi9XMsXEN2wHK5siJV/dw/EWs1SyA1wDU7eFELkQ0mrTBJ5E9xb4wk4IfsUXFHiDohEX7lLGaelkg9+Sy6OnqYq/qqoKdOoJ2kA3yL6Yjl86nDeQ9KAcOXmyb+eqm1L3k+E30WLFKjvwrkqnat5DaJsUbq7W2Aw9QyIkj6hK/Ay2639QfmHkLNEhFdw6fj4j1J1HOJ+j1Auu4g1S1iTtk2/TGPqD6DZjWNXjCkLLhfa5n5EJGyQozy8pf55NOBb0bLvLzQBy5iNuNBRggdgew3uzPCdNn14pYV3jcLLWeNfYqSafAsuYuPuqLZ449tzP0Kvxj7Pnr2yxq0WQBdLWkiMNEIEuzGe5rdh3AMCjcx+wZGGJPhTIQCenjiVmMSzlWPi/gUKc15zV9A4WjX96aG9KdxYeZ1SL+JaV4I2BLDlfWTyXtfoSAHvANMWece5A+1DMDUrelRskq0hT87FammYoiFfLd/2gjjbymzMJ8vrSBmhQ79DgyBMOYgTmA

Hi,

I defined a function about (A: Type), (f: A -> A), and (T: A -> Type) as follows.

Definition omega (a: A): T (f a) := (* _expression_ *).

I also took (g: A -> A) and proved the following lemma.

Lemma f_a_eq_g_a : forall (a: A), f a = g a.

Now, I want to treat (omega a) as a value in (T (g a)). Is there any easy way to do this?

Regards,

Koki

[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