How to define list of natural numbers without gaps in Coq?
For example [2, 1, 3] is valid list, but [5, 1, 3] is not because it have two gaps: between 1 and 3, 3 and 5.
I have try to ask Google, but nothing similar was found
List without gaps in Coq
45 views Asked by vzhilin At
1
There are 1 answers
Related Questions in COQ
- Coq : mutually recursive definitions with [mrec] in InteractionTrees Library
- Is there a function that returns a list of values with specific type in OCaml?
- How to prove (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)?
- Showing polynomial equality in coq/ssreflect
- Syntax of the case tactic in coq
- Why assuming singleton elimination and definitional proof irrelevance leads to UIP, in Coq?
- Understanding nat_ind2 in Logical Foundations
- What `dependent induction` tactic does in Coq and how to use it
- Split multiple conjuncts in the goal
- Coq can't define an inductive proposition
- Coq Decreasing Argument mapping
- The `specialize` tatic in Coq does not work well with typeclasses?
- Multiple Assignements in a Coq Map to the same value
- Decider for lists In Fixpoint
- VSCoq Error: Connection to server got closed. Server will not be restarted
Related Questions in DEPENDENT-TYPE
- Notation for functions returning dependent types
- how to create a type that contains an array of a specific length, in F#
- Could TypeScript model this function if it had dependent types?
- Dependent equality with 2 different type functions
- How can I prove dependent function types equal in Agda?
- In Scala 3, should 2 dependent types that depends on 2 equal & singleton objects perceived to be equal? Why or why not?
- How do I efficiently add existentially typed safe money values?
- Why can some disjoint and exhaustive patterns not be represented as definitional equalities?
- What does the pound sign mean in Idris 2?
- writing a dependent type in agda to guarantee a list is sorted
- In Scala 3 (dotty) or Scala 2, how to make dependent types transitive?
- Updating a dependently typed field without updating what it depends on
- Equality of coinductive types
- How to deal with non-termination error in Cubical Agda
- List without gaps in Coq
Related Questions in TYPE-THEORY
- TypeScript recursive union function type
- What is the paradigm of wrapping generic parameters into nested structures called?
- Parity of nested function type and recursive call
- Why can some disjoint and exhaustive patterns not be represented as definitional equalities?
- List without gaps in Coq
- In cubical type theory, why are there function types that accept intervals as arguments when there are already a path type?
- How to prove Theorem euclid_gcd : forall a b z, euclid a b z -> gcd a b z. using coq?
- Rust is the automatic dereference of Box types prohibative?
- Is there a library for sets that works with bool in Coq?
- Type theory with an Any/Variant type
- Why can't all existential binders be replaced by unique constants during skolemization?
- In intuitionistic type theory, can any proof written in CoC be rewritten in system λP2? Or, does CoC = λP2?
- It is possible to define a function in haskell that takes one parameter, ignores it, and returns itself?
- Why can't I define this rewrite rule for type elimination of proof-irrelevant disjunctions in Agda
- Non-determinism on a set defined by the characteristic function
Popular Questions
- How do I undo the most recent local commits in Git?
- How can I remove a specific item from an array in JavaScript?
- How do I delete a Git branch locally and remotely?
- Find all files containing a specific text (string) on Linux?
- How do I revert a Git repository to a previous commit?
- How do I create an HTML button that acts like a link?
- How do I check out a remote Git branch?
- How do I force "git pull" to overwrite local files?
- How do I list all files of a directory?
- How to check whether a string contains a substring in JavaScript?
- How do I redirect to another webpage?
- How can I iterate over rows in a Pandas DataFrame?
- How do I convert a String to an int in Java?
- Does Python have a string 'contains' substring method?
- How do I check if a string contains a specific word?
Popular Tags
Trending Questions
- UIImageView Frame Doesn't Reflect Constraints
- Is it possible to use adb commands to click on a view by finding its ID?
- How to create a new web character symbol recognizable by html/javascript?
- Why isn't my CSS3 animation smooth in Google Chrome (but very smooth on other browsers)?
- Heap Gives Page Fault
- Connect ffmpeg to Visual Studio 2008
- Both Object- and ValueAnimator jumps when Duration is set above API LvL 24
- How to avoid default initialization of objects in std::vector?
- second argument of the command line arguments in a format other than char** argv or char* argv[]
- How to improve efficiency of algorithm which generates next lexicographic permutation?
- Navigating to the another actvity app getting crash in android
- How to read the particular message format in android and store in sqlite database?
- Resetting inventory status after order is cancelled
- Efficiently compute powers of X in SSE/AVX
- Insert into an external database using ajax and php : POST 500 (Internal Server Error)
You could say that a list of length
nis without gaps iff its sorted version is equal to the list of naturals from 1 ton. If need be, this could be packaged in a dependent record, with the list and its no-gap property as fields.