coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] height of derivations

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] height of derivations
Date: Thu, 25 Jul 2019 08:10:47 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1;spf=pass smtp.mailfrom=anu.edu.au;dmarc=pass action=none header.from=anu.edu.au;dkim=pass header.d=anu.edu.au;arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=ikJQJcE9yaTlTcdi+KbsK8Chpa+C2rWyVBdcLJYUNHQ=; b=kj3B++Y4wzVBs4dic5u6rrLdrWZsR5a37EIVC/xSOVlgN38dfPbgwDTmk1B5C9RtwvSbw4lw7qxPUAVJygCJrqPVbeg3dzoPPinNbar+FciKw65ykjYv8lSk2Xc8dC871GOvLKFpdfFSAAm3h3+gcB1VSsXs5zi+sLxZzv5k+qmxZc8mWOA7lARnHRdbK/wkRPp2c6obyCCGEjp0onaytxYWK2n4bytsCC4/L71q8+UoQAs+S2iSA2787dRuU04fx0bGaJiSIJTaXQjKJjgyqUWVpc+ArPHtLsyvepEXnn+c0O0sJ25OIh5rJBqf0BHppGIEn2CBkeQvy1qHNTWDWg==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=EGIr6fo0c2cEq7MCayuHqHTDuCWaSsBbl9KPVVJcClqYGOVuuvNzFxlZ8NgT96DNBKgSYBHOlqi6LWQGmhjNZIC/YK/lxfkwMSVhlZzns5irLBc/3rp+HYKSmIMpQy/Kkidx3Cvl07m0jUKtPMWVTPW06OaNvlbVF3C4F3KRqncGEuO6ma/9P/tlV9V97o+sTzAuafVcPn8Pz4vHKkfR5KaVY3L/OIvFwYetkAIkBKNpo0mlAYA0D3tiCI8hInc7kGk6YhDoXjiP+7Q8GrtmZv75R6Y7uK5TWCHFNdL0DyWMOBJ2oPpT/owfV/pBCkWc62RXoovUWPrMCk80GLdDmQ==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:heO/HBxJ6j9NWuXXCy+O+j09IxM/srCxBDY+r6Qd2+IUIJqq85mqBkHD//Il1AaPAdyBraIdwLOM6ejJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVmjaxe7B/IAi5oQnMqMUan5ZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8JwkqxVvQ6hqRJ8zY7VfI6bO/Vxc7jBfdwBX2dNQtpdWzBDD466coABD/ABPeFdr4Tlo1UBswG+ChepBOLv1zRGiGX53KMh0+QmFwHNwQstEdYQv3TOstr1MacTXfq7wqbSwzTDdPRW2THm5YfSdBAhvOuAUqxtfsrM00UgDR7Fg0yWpIf4PD2VzvwAvmeH4+Z6SO6jl2wqpxtsrjWhxMogkJTFipwWx1zc6Cl0wJo5KcemREJnb9OoCoVcuzyGO4dsX88vTWVltD40yrIYupO3YC0HxZE6yxPQb/GKc42F7xziWeuQIjp1gWlqdbyxihu3/kWs1OPxW8ay3V1XtCRKiMPMuWoI1xHL6siIVP99/kC51DuT2Q/d9/1ILV0tmaTGKZEszKc8lp0IvkvdBCP2n1j2jLONeUUj5+io7fnobq/+pp+GMI90lh/xPbgymsy+BuQ4NBICX2+G+eSg0L3j+kr5QLZQgvIqlanZtYjWJcUdpqGnHw9Yyoku5wqlAzu7zNgVn2MLIE9LdR+FlYTlJk/CLfPgAfe6mVuskTNrx/7cPr3mB5XANnzNn6n7fblj7k5dyBA/w95F6JNaEbEBJ/TzV1Tru9zeEx81KRK7zPv6CNlnzIweRHqDArWFP6PKrV+I+uUvLvGQa48SoTbxMuQq5/rzjXAiglIdZqmo3Z4PaH+iBPhmIkOZYWDtgtgbC2sKsBA+H6TWjwjIWjlKIn22QqgU5zchCYvgA52JDtSmh6XE1yOmFLVXYHpHAxaCCyG7WZ+DXqIuZTifJ94pvjUbTr+nA9sD2AujsR6857N4Ne3S0iQeqNTu2MUz7vCFxkJ6ziB9E8nIizLFdGpzhG5dH2ZnjpA6mlR0zxK46YY9hvVZEdJJ4PYQCFUzM4OawuBnTdnvCFuYIoW5DW2+S9DjOgkfC8oryoZUMU97BpOvgg2F1jf4W+ZIxYzOP4Q99+fn51a0J8t5zCqZhoActAF/B/B+biihjKM58BXPDYnUlUnfj7ytaakXwC/K8iGE0HaKu0ZbFgV3VPecUA==

Hi,

I'm implementing some netalogic in Coq, in which it is easy to say. (for
example)

is_derivable A -> is_derivable B -> is_derivable (A and B)

Unlike some other proof logics, we get an object which represents the
actual proof (whose type is is_derivable (A and B)), and potentially we
should be able to define the height or size (number of steps) of the
proof tree involved.

However, whereas the natural view of the type of is_derivable would be
formula -> Prop, I find that to define the height of the proof object I
need to make the type of is_derivable formula -> Type

Then I find that whereas my initial version (that is, the Prop version)
of is_derivable involved standard stuff like Forall and In (of types ...
-> Prop), I need versions of these with types --- -> Type. Examples
shown below.

My questions are:
- does this sort of thing already exist (maybe under a different
name), and
- is there an easier way than defining new versions of these standard
library functions?

thanks

Jeremy

InT_nilE: forall (A : Type) (a : A) (any : Type), InT (a : A) [] -> any
InT_eq: forall (A : Type) (a : A) (l : list A), InT a (a :: l)
InT_cons: forall (A : Type) (a b : A) (l : list A), InT a l -> InT a (b
:: l)
InT_eq': forall (A : Type) (a b : A) (l : list A), b = a -> InT a (b :: l)
InT_appL: forall (A : Type) (a : A) (X Y : list A),
InT (a : A) X -> InT a (X ++ Y)
InT_appR: forall (A : Type) (a : A) (X Y : list A),
InT (a : A) Y -> InT a (X ++ Y)

ForallT_nil: forall (A : Type) (P : A -> Type), ForallT P []
ForallT_inv: forall (A : Type) (P : A -> Type) (a : A) (l : list A),
ForallT P (a :: l) -> P a
ForallT_single: forall (A : Type) (P : A -> Type) (x : A),
iffT (ForallT P [x]) (P x)
ForallT_cons: forall (A : Type) (P : A -> Type) (x : A) (l : list A),
P x -> ForallT P l -> ForallT P (x :: l)
ForallT_forall: forall (A : Type) (P : A -> Type) (l : list A),
iffT (ForallT P l) (forall x : A, InT x l -> P x)
ForallT_cons_inv: forall (A : Type) (P : A -> Type) (x : A) (l : list A),
ForallT P (x :: l) -> P x * ForallT P l
ForallT_cons_iff: forall (A : Type) (P : A -> Type) (x : A) (l : list A),
iffT (ForallT P (x :: l)) (P x * ForallT P l)

[Coq-Club] height of derivations, Jeremy Dawson, 07/25/2019
- Re: [Coq-Club] height of derivations, Dominique Larchey-Wendling, 07/25/2019
- Re: [Coq-Club] height of derivations, Matthieu Sozeau, 07/25/2019