Skip to Content.
Sympa Menu

coq-club - [Coq-Club] height of derivations

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] height of derivations


Chronological Thread 
  • 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)




Archive powered by MHonArc 2.6.18.

Top of Page