archive-nl.com » NL » R » ROBBERTKREBBERS.NL

Total: 145

Choose link from "Titles, links and description words view":

Or switch to "Titles and links view".
  • Robbert Krebbers
    In ITP volume 8558 of LNCS pages 543 548 pdf at publisher slides coq sources Robbert Krebbers An operational and axiomatic semantics for non determinism and sequence points in C In POPL pages 101 112 pdf at publisher slides coq sources 2013 Robbert Krebbers Aliasing restrictions of C11 formalized in Coq In CPP volume 8307 of LNCS pages 50 65 pdf at publisher slides coq sources Robbert Krebbers and Freek Wiedijk Separation Logic for Non local Control Flow and Block Scope Variables In FoSSaCS volume 7794 of LNCS pages 257 272 Awarded best student contribution pdf at publisher slides coq sources documentation Herman Geuvers Robbert Krebbers and James McKinna The λμT calculus In volume 164 issue 6 of APAL pages 676 701 pdf at publisher Robbert Krebbers and Bas Spitters Type classes for efficient exact real arithmetic in Coq In volume 9 issue 1 of LMCS pages 1 27 pdf at publisher coq sources 2012 Robbert Krebbers A call by value λ calculus with lists and control In CL C volume 97 of EPTCS pages 19 33 pdf at publisher slides 2011 Herman Geuvers and Robbert Krebbers The correctness of Newman s typability algorithm and some of its extensions In volume 412 of TCS pages 3242 3261 pdf at publisher Robbert Krebbers and Bas Spitters Computer certified efficient exact reals in Coq In CICM volume 6824 of LNAI pages 90 103 pdf at publisher slides coq sources Robbert Krebbers and Freek Wiedijk A Formalization of the C99 Standard in HOL Isabelle and Coq In CICM volume 6824 of LNAI pages 297 299 pdf at publisher poster slides 2010 Robbert Krebbers A formalization of Γ in Coq Note pdf coq formalization Herman Geuvers Robbert Krebbers James McKinna and Freek Wiedijk Pure Type Systems without Explicit Contexts In LFMTP volume 34 of

    Original URL path: http://robbertkrebbers.nl/ (2015-08-10)
    Open archived version from archive


  • The CH₂O formalization of ISO C11
    257 272 2013 Awarded best student contribution pdf at publisher slides coq sources Robbert Krebbers and Freek Wiedijk A Formalization of the C99 Standard in HOL Isabelle and Coq In CICM volume 6824 of LNAI pages 297 299 2011 pdf at publisher poster slides Download The most recent version of the Coq source code of this development can be downloaded here Use scons j num cores to compile the development This yields an executable called ch2o that can be used to test the CH 2 O semantics against actual C source files Table of contents Prelude base interfaces notations and general theorems tactics general purpose tactics proof irrel facts about proof irrelevant types propositions decidable theorems on decidable structures orders theorems on ordered structures option the option monad and various theorems on the option type error the error monad list miscellaneous definitions and theorems on lists streams miscellaneous definitions and theorems on streams vector miscellaneous definitions and theorems on vectors numbers miscellaneous facts on nat N and Z ars theorems and definitions on abstract rewriting systems collections definitions theorems and tactics for collections fin collections theorems on finite collections listset finite set implementation using unordered lists fresh numbers generation of fresh numbers prelude exports all of the above Finite maps fin maps an interface and properties of finite maps fin map dom an interface and theorems for the domain function of finite maps mapset finite maps give rise to finite sets with extensional equality natmap pmap nmap zmap and stringmap finite maps indexed by nat positive N Z and string hashset simple hashsets using finite maps over positive Type system and integers integer coding abstract interface for integer representations integer operations abstract interface for integer operations type classes classes to overload notations for typing judgments types C types and type environments type environment abstract interface for implementation defined properties architecture spec type environment specifications based on concrete architectures architectures some specific architectures ilp32 llp64 and lp64 Permissions and separation algebras separation abstract interface and properties of separation algebras separation instances boolean fractional counting lockable and tagged separation algebras permissions the CH 2 O permission system as a separation algebra ctrees separation algebra of abstract trees representing memory objects cmap separation algebra of abstract forests representing memories Memory model memory basics basic definitions of the memory model references paths through types ctrees addresses refinements addresses into the memory pointers refinements definition of pointers address or NULL pointer bits refinements pointer fragment bits pointer with index bits refinements symbolic bits 0 1 indeterminate or pointer fragment permission bits refinements and separation bits annotated with permissions memory trees refinements and separation memory operations on C trees memory map refinements and separation memory operations on C maps base values refinements base values void indeterminate integer or pointer values refinements and separation abstract values base value array struct or union memory refinements and separation the CH 2 O memory model and its operations aliasing abstract proof showing that type based alias analysis is allowed constant

    Original URL path: http://robbertkrebbers.nl/research/ch2o/ (2015-08-10)
    Open archived version from archive

  • Computer certified efficient exact reals in Coq
    LMCS pdf Robbert Krebbers and Bas Spitters Computer certified efficient exact reals in Coq In CICM volume 6824 of LNAI pages 90 103 pdf slides Slides TYPES September 9 2011 Bergen Norway pdf The Coq Workshop August 26 2011 Nijmegen the Netherlands pdf Conference on Intelligent Computer Mathematics July 23 2011 Bertinoro Italy pdf Brouwer seminar March 22 2011 Radboud University Nijmegen the Netherlands pdf Workshop on reification and generic

    Original URL path: http://robbertkrebbers.nl/research/reals/ (2015-08-10)
    Open archived version from archive

  • A formalization of Gamma infinity in Coq
    contexts A typing judgment in Γ is of the shape A B while an ordinary judgment is of the shape Γ A B This approach of Geuvers et al makes a bridge between traditional logic and type theory In the former free variables are really free and contexts are non explicit as in Γ Furthermore Γ could make it possible to create a stateless version of an LCF style prover

    Original URL path: http://robbertkrebbers.nl/research/gammainf/ (2015-08-10)
    Open archived version from archive

  • Module base
    1 q 1 at level 70 C scope Infix 2 Forall2 λ p q p 2 q 2 at level 70 C scope Hint Extern 0 reflexivity Hint Extern 0 reflexivity Hint Extern 0 reflexivity Class SubsetEqE E A subseteqE E relation A Instance Params subseteqE 4 Notation X Γ Y subseteqE Γ X Y at level 70 format X Γ Y C scope Notation Γ subseteqE Γ only parsing Γ at level 1 C scope Notation X Γ Y X Γ Y at level 70 format X Γ Y C scope Notation Γ λ X Y X Γ Y only parsing Γ at level 1 C scope Notation Xs Γ Ys Forall2 Γ Xs Ys at level 70 format Xs Γ Ys C scope Notation Γ Forall2 Γ only parsing Γ at level 1 C scope Notation X Γ1 Γ2 Γ3 Y subseteqE pair Γ1 Γ2 Γ3 X Y at level 70 format X Γ1 Γ2 Γ3 Y C scope Notation Γ1 Γ2 Γ3 subseteqE pair Γ1 Γ2 Γ3 only parsing Γ1 at level 1 C scope Notation X Γ1 Γ2 Γ3 Y X pair Γ1 Γ2 Γ3 Y at level 70 format X Γ1 Γ2 Γ3 Y C scope Notation Γ1 Γ2 Γ3 λ X Y X pair Γ1 Γ2 Γ3 Y only parsing C scope Notation Xs Γ1 Γ2 Γ3 Ys Forall2 pair Γ1 Γ2 Γ3 Xs Ys at level 70 format Xs Γ1 Γ2 Γ3 Ys C scope Notation Γ1 Γ2 Γ3 Forall2 pair Γ1 Γ2 Γ3 only parsing Γ1 at level 1 C scope Hint Extern 0 reflexivity Definition strict A R relation A relation A λ X Y R X Y R Y X Instance Params strict 2 Infix strict at level 70 C scope Notation strict only parsing C scope Notation X strict X only parsing C scope Notation X λ Y Y X only parsing C scope Notation X Y X Y at level 70 C scope Notation λ X Y X Y only parsing C scope Notation X λ Y X Y only parsing C scope Notation X λ Y Y X only parsing C scope The class Lexico A is used for the lexicographic order on A This order is used to create finite maps finite sets etc and is typically different from the order Class Lexico A lexico relation A Class ElemOf A B elem of A B Prop Instance Params elem of 3 Infix elem of at level 70 C scope Notation elem of only parsing C scope Notation x elem of x only parsing C scope Notation X λ x elem of x X only parsing C scope Notation x X x X at level 80 C scope Notation λ x X x X only parsing C scope Notation x λ X x X only parsing C scope Notation X λ x x X only parsing C scope Class Disjoint A disjoint A A Prop Instance Params disjoint 2 Infix disjoint at level 70 C scope Notation disjoint only parsing C scope Notation X disjoint X only parsing C scope Notation X λ Y Y X only parsing C scope Infix Forall2 at level 70 C scope Notation Forall2 only parsing C scope Infix Forall2 at level 70 C scope Infix 1 Forall2 λ p q p 1 q 1 at level 70 C scope Infix 2 Forall2 λ p q p 2 q 2 at level 70 C scope Infix 1 Forall2 λ p q p 1 q 1 at level 70 C scope Infix 2 Forall2 λ p q p 2 q 2 at level 70 C scope Hint Extern 0 symmetry eassumption Hint Extern 0 symmetry eassumption Class DisjointE E A disjointE E A A Prop Instance Params disjointE 4 Notation X Γ Y disjointE Γ X Y at level 70 format X Γ Y C scope Notation Γ disjointE Γ only parsing Γ at level 1 C scope Notation Xs Γ Ys Forall2 Γ Xs Ys at level 70 format Xs Γ Ys C scope Notation Γ Forall2 Γ only parsing Γ at level 1 C scope Notation X Γ1 Γ2 Γ3 Y disjoint pair Γ1 Γ2 Γ3 X Y at level 70 format X Γ1 Γ2 Γ3 Y C scope Notation Xs Γ1 Γ2 Γ3 Ys Forall2 disjoint pair Γ1 Γ2 Γ3 Xs Ys at level 70 format Xs Γ1 Γ2 Γ3 Ys C scope Hint Extern 0 symmetry eassumption Class DisjointList A disjoint list list A Prop Instance Params disjoint list 2 Notation Xs disjoint list Xs at level 20 format Xs C scope Section disjoint list Context Disjoint A Union A Empty A Inductive disjoint list default DisjointList A disjoint nil 2 nil A disjoint cons 2 X A Xs list A X Xs Xs X Xs Global Existing Instance disjoint list default Lemma disjoint list nil nil A True Proof split constructor Qed Lemma disjoint list cons X Xs X Xs X Xs Xs Proof split inversion clear 1 auto intros constructor auto Qed End disjoint list Class Filter A B filter P A Prop x Decision P x B B Monadic operations We define operational type classes for the monadic operations bind join and fmap We use these type classes merely for convenient overloading of notations and do not formalize any theory on monads we do not even define a class with the monad laws Class MRet M Type Type mret A A M A Instance Params mret 3 Arguments mret Class MBind M Type Type mbind A B A M B M A M B Arguments mbind Instance Params mbind 5 Class MJoin M Type Type mjoin A M M A M A Instance Params mjoin 3 Arguments mjoin Class FMap M Type Type fmap A B A B M A M B Instance Params fmap 6 Arguments fmap Class OMap M Type Type omap A B A option B M A M B Instance Params omap 6 Arguments omap Notation m f mbind f m at level 60 right associativity C scope Notation m λ f mbind f m only parsing C scope Notation f mbind f only parsing C scope Notation λ m f mbind f m only parsing C scope Notation x y z y λ x z at level 65 next at level 35 only parsing right associativity C scope Infix fmap at level 60 right associativity C scope Notation x1 x2 y z y λ x let x1 x2 x in z at level 65 next at level 35 only parsing right associativity C scope Notation x1 x2 x3 y z y λ x let x1 x2 x3 x in z at level 65 next at level 35 only parsing right associativity C scope Notation x1 x2 x3 x4 y z y λ x let x1 x2 x3 x4 x in z at level 65 next at level 35 only parsing right associativity C scope Notation x1 x2 x3 x4 x5 y z y λ x let x1 x2 x3 x4 x5 x in z at level 65 next at level 35 only parsing right associativity C scope Notation x1 x2 x3 x4 x5 x6 y z y λ x let x1 x2 x3 x4 x5 x6 x in z at level 65 next at level 35 only parsing right associativity C scope Notation ps 1 fmap M list fst ps at level 10 format ps 1 Notation ps 2 fmap M list snd ps at level 10 format ps 2 Class MGuard M Type Type mguard P dec Decision P A P M A M A Arguments mguard Notation guard P o mguard P λ o at level 65 next at level 35 only parsing right associativity C scope Notation guard P as H o mguard P λ H o at level 65 next at level 35 only parsing right associativity C scope Operations on maps In this section we define operational type classes for the operations on maps In the file fin maps we will axiomatize finite maps The function look up m k should yield the element at key k in m Class Lookup K A M Type lookup K M option A Instance Params lookup 4 Notation m i lookup i m at level 20 C scope Notation lookup only parsing C scope Notation m λ i m i only parsing C scope Notation i lookup i only parsing C scope Arguments lookup simpl nomatch The function insert k a m should update the element at key k with value a in m Class Insert K A M Type insert K A M M Instance Params insert 4 Notation k a insert k a at level 5 right associativity format k a C scope Arguments insert simpl nomatch The function delete delete k m should delete the value at key k in m If the key k is not a member of m the original map should be returned Class Delete K M Type delete K M M Instance Params delete 3 Arguments delete simpl nomatch The function alter f k m should update the value at key k using the function f which is called with the original value Class Alter K A M Type alter A A K M M Instance Params alter 5 Arguments alter simpl nomatch The function alter f k m should update the value at key k using the function f which is called with the original value at key k or None if k is not a member of m The value at k should be deleted if f yields None Class PartialAlter K A M Type partial alter option A option A K M M Instance Params partial alter 4 Arguments partial alter simpl nomatch The function dom C m should yield the domain of m That is a finite collection of type C that contains the keys that are a member of m Class Dom M C Type dom M C Instance Params dom 3 Arguments dom simpl nomatch clear implicits The function merge f m1 m2 should merge the maps m1 and m2 by constructing a new map whose value at key k is f m1 k m2 k Class Merge M Type Type merge A B C option A option B option C M A M B M C Instance Params merge 4 Arguments merge simpl nomatch The function union with f m1 m2 is supposed to yield the union of m1 and m2 using the function f to combine values of members that are in both m1 and m2 Class UnionWith A M Type union with A A option A M M M Instance Params union with 3 Arguments union with simpl nomatch Similarly for intersection and difference Class IntersectionWith A M Type intersection with A A option A M M M Instance Params intersection with 3 Arguments intersection with simpl nomatch Class DifferenceWith A M Type difference with A A option A M M M Instance Params difference with 3 Arguments difference with simpl nomatch Definition intersection with list IntersectionWith A M f A A option A M list M M fold right intersection with f Arguments intersection with list Class LookupE E K A M Type lookupE E K M option A Instance Params lookupE 6 Notation m Γ i lookupE Γ i m at level 20 format m Γ i C scope Notation Γ lookupE Γ only parsing Γ at level 1 C scope Arguments lookupE simpl nomatch Class InsertE E K A M Type insertE E K A M M Instance Params insert 6 Notation k a Γ insertE Γ k a at level 5 right associativity format k a Γ C scope Arguments insertE simpl nomatch Common properties These operational type classes allow us to refer to common mathematical properties in a generic way For example for injectivity of k it allows us to write injective k instead of app inv head k Class Injective A B R relation A S relation B f A B Prop injective x y S f x f y R x y Class Injective2 A B C R1 relation A R2 relation B S relation C f A B C Prop injective2 x1 x2 y1 y2 S f x1 x2 f y1 y2 R1 x1 y1 R2 x2 y2 Class Cancel A B S relation B f A B g B A Prop cancel x S f g x x Class Surjective A B R relation B f A B surjective y x R f x y Class Idempotent A R relation A f A A A Prop idempotent x R f x x x Class Commutative A B R relation A f B B A Prop commutative x y R f x y f y x Class LeftId A R relation A i A f A A A Prop left id x R f i x x Class RightId A R relation A i A f A A A Prop right id x R f x i x Class Associative A R relation A f A A A Prop associative x y z R f x f y z f f x y z Class LeftAbsorb A R relation A i A f A A A Prop left absorb x R f i x i Class RightAbsorb A R relation A i A f A A A Prop right absorb x R f x i i Class LeftDistr A R relation A f g A A A Prop left distr x y z R f x g y z g f x y f x z Class RightDistr A R relation A f g A A A Prop right distr y z x R f g y z x g f y x f z x Class AntiSymmetric A R S relation A Prop anti symmetric x y S x y S y x R x y Class Total A R relation A total x y R x y R y x Class Trichotomy A R relation A trichotomy x y R x y x y R y x Class TrichotomyT A R relation A trichotomyT x y R x y x y R y x Arguments irreflexivity Arguments injective Arguments injective2 Arguments cancel Arguments surjective Arguments idempotent Arguments commutative Arguments left id Arguments right id Arguments associative Arguments left absorb Arguments right absorb Arguments left distr Arguments right distr Arguments anti symmetric Arguments total Arguments trichotomy Arguments trichotomyT Instance id injective A Injective id A Proof intros auto Qed The following lemmas are specific versions of the projections of the above type classes for Leibniz equality These lemmas allow us to enforce Coq not to use the setoid rewriting mechanism Lemma idempotent L A f A A A Idempotent f x f x x x Proof auto Qed Lemma commutative L A B f B B A Commutative f x y f x y f y x Proof auto Qed Lemma left id L A i A f A A A LeftId i f x f i x x Proof auto Qed Lemma right id L A i A f A A A RightId i f x f x i x Proof auto Qed Lemma associative L A f A A A Associative f x y z f x f y z f f x y z Proof auto Qed Lemma left absorb L A i A f A A A LeftAbsorb i f x f i x i Proof auto Qed Lemma right absorb L A i A f A A A RightAbsorb i f x f x i i Proof auto Qed Lemma left distr L A f g A A A LeftDistr f g x y z f x g y z g f x y f x z Proof auto Qed Lemma right distr L A f g A A A RightDistr f g y z x f g y z x g f y x f z x Proof auto Qed Axiomatization of ordered structures The classes PreOrder PartialOrder and TotalOrder use an arbitrary relation R instead of to support multiple orders on the same type Class PartialOrder A R relation A Prop partial order pre PreOrder R partial order anti symmetric AntiSymmetric R Class TotalOrder A R relation A Prop total order partial PartialOrder R total order trichotomy Trichotomy strict R We do not use a setoid equality in the following interfaces to avoid the need for proofs that the relations and operations are proper Instead we define setoid equality generically λ X Y X Y Y X Class EmptySpec A Empty A SubsetEq A Prop subseteq empty X X Class JoinSemiLattice A SubsetEq A Union A Prop join semi lattice pre PreOrder union subseteq l X Y X X Y union subseteq r X Y Y X Y union least X Y Z X Z Y Z X Y Z Class MeetSemiLattice A SubsetEq A Intersection A Prop meet semi lattice pre PreOrder intersection subseteq l X Y X Y X intersection subseteq r X Y X Y Y intersection greatest X Y Z Z X Z Y Z X Y Class Lattice A SubsetEq A Union A Intersection A Prop lattice join JoinSemiLattice A lattice meet MeetSemiLattice A lattice distr X Y Z X Y X Z X Y Z Axiomatization of collections The class SimpleCollection A C axiomatizes a collection of type C with elements of type A Instance Params map 3 Class SimpleCollection A C ElemOf A C Empty C Singleton A C Union C Prop not elem of empty x A x elem of singleton x y A x y x y elem of union X Y x A x X Y x X x Y Class Collection A C ElemOf A C Empty C Singleton A C Union C Intersection C Difference C Prop collection simple SimpleCollection A C elem of intersection X Y x A x X Y x X

    Original URL path: http://robbertkrebbers.nl/research/ch2o/base.html (2015-08-10)
    Open archived version from archive

  • Module tactics
    H end Ltac block hyps repeat on hyps fun H match type of H with block idtac T change block T in H end Ltac unblock hyps unfold block in The tactic injection H is a variant of injection that introduces the generated equalities Ltac injection H block goal injection H clear H intros H intros unblock goal The tactic simplify equality repeatedly substitutes discriminates and injects equalities and tries to contradict impossible inequalities Ltac fold classes repeat match goal with appcontext F progress match type of F with FMap change F with fmap F repeat change fmap fmap F with fmap F MBind change F with mbind F repeat change mbind mbind F with mbind F OMap change F with omap F repeat change omap omap F with omap F Alter change F with alter F repeat change alter alter F with alter F end end Ltac fold classes hyps H repeat match type of H with appcontext F progress match type of F with FMap change F with fmap F in H repeat change fmap fmap F with fmap F in H MBind change F with mbind F in H repeat change mbind mbind F with mbind F in H OMap change F with omap F in H repeat change omap omap F with omap F in H Alter change F with alter F in H repeat change alter alter F with alter F in H end end Tactic Notation csimpl in hyp H try progress simpl in H fold classes hyps H Tactic Notation csimpl try progress simpl fold classes Tactic Notation csimpl in repeat on hyps fun H csimpl in H csimpl Ltac simplify equality repeat match goal with H by destruct H H False by destruct H H x subst x H x subst x H discriminate H H f f apply injective f in H H f f apply injective2 f in H destruct H H f f injection H H f f injection H H f f injection H H f f injection H H f f injection H H f f injection H H x x clear H H1 o Some x H2 o Some y assert y x by congruence clear H2 H1 o Some x H2 o None congruence end Ltac simplify equality repeat progress csimpl in simplify equality Ltac f equal csimpl in f equal Ltac f lia repeat lazymatch goal with eq BinNums Z lia eq nat lia f equal end Ltac f lia csimpl in f lia Given a tactic tac2 generating a list of terms iter tac1 tac2 runs tac x for each element x until tac x succeeds If it does not suceed for any element of the generated list the whole tactic wil fail Tactic Notation iter tactic tac tactic l let rec go l match l with x l tac x go l end in go l Given H A 1 A n B where each A i is non dependent the tactic

    Original URL path: http://robbertkrebbers.nl/research/ch2o/tactics.html (2015-08-10)
    Open archived version from archive

  • Module proof_irrel
    A B Type ProofIrrel A ProofIrrel B ProofIrrel A B Proof intros by f equal Qed Instance eq pi A x y A Decision x y x y A ProofIrrel x y Proof intros apply eq proofs unicity intros x y destruct decide x y tauto Qed Instance Is true pi b bool ProofIrrel Is true b Proof destruct b simpl apply Qed Lemma sig eq pi P A Prop

    Original URL path: http://robbertkrebbers.nl/research/ch2o/proof_irrel.html (2015-08-10)
    Open archived version from archive

  • Module decidable
    the refine tactic Notation swap if S match S with left H right H right H left H end Notation cast if S if S then left else right Notation cast if and S1 S2 if S1 then cast if S2 else right Notation cast if and3 S1 S2 S3 if S1 then cast if and S2 S3 else right Notation cast if and4 S1 S2 S3 S4 if S1 then cast if and3 S2 S3 S4 else right Notation cast if and5 S1 S2 S3 S4 S5 if S1 then cast if and4 S2 S3 S4 S5 else right Notation cast if and6 S1 S2 S3 S4 S5 S6 if S1 then cast if and5 S2 S3 S4 S5 S6 else right Notation cast if or S1 S2 if S1 then left else cast if S2 Notation cast if or3 S1 S2 S3 if S1 then left else cast if or S2 S3 Notation cast if not or S1 S2 if S1 then cast if S2 else left Notation cast if not S if S then right else left We can convert decidable propositions to booleans Definition bool decide P Prop dec Decision P bool if dec then true else false Lemma bool decide reflect P dec Decision P reflect P bool decide P Proof unfold bool decide destruct dec by left by right Qed Tactic Notation case bool decide as ident Hd match goal with H context bool decide P dec destruct decide bool decide reflect P dec as Hd context bool decide P dec destruct decide bool decide reflect P dec as Hd end Tactic Notation case bool decide let H fresh in case bool decide as H Lemma bool decide spec P Prop dec Decision P bool decide P P Proof unfold bool decide by destruct dec Qed Lemma bool decide unpack P Prop dec Decision P bool decide P P Proof by rewrite bool decide spec Qed Lemma bool decide pack P Prop dec Decision P P bool decide P Proof by rewrite bool decide spec Qed Lemma bool decide true P Prop Decision P P bool decide P true Proof by case bool decide Qed Lemma bool decide false P Prop Decision P P bool decide P false Proof by case bool decide Qed Lemma bool decide iff P Q Prop Decision P Decision Q P Q bool decide P bool decide Q Proof repeat case bool decide tauto Qed Decidable Sigma types Leibniz equality on Sigma types requires the equipped proofs to be equal as Coq does not support proof irrelevance For decidable we propositions we define the type dsig P whose Leibniz equality is proof irrelevant That is x y dsig P x y x y Due to the absence of universe polymorpic definitions we also define a variant dsigS for types in Set Definition dsig P A Prop x A Decision P x x bool decide P x Definition dsigS A Set P A Prop x A Decision P x Set

    Original URL path: http://robbertkrebbers.nl/research/ch2o/decidable.html (2015-08-10)
    Open archived version from archive