Coq es un demostrador de teoremas interactivo.
Al codificar una lógica en un asistente de prueba tales como Coq o Isabelle, una elección debe ser hecha entre usar un poco profunda y una profunda incrustación. En una incrustación superficial, las fórmulas lógicas se escriben directamente en la lógica del probador de teoremas, mientras que en una...
Voy a repasar las notas del curso en CIS 500: Fundamentos de software y los ejercicios son muy divertidos. Solo estoy en el tercer conjunto de ejercicios, pero me gustaría saber más sobre lo que sucede cuando uso tácticas para probar cosas comoforall (n m : nat), n + n = m + m -> n =...
Coq tiene un tipo de Prop. De prueba proposiciones irrelevantes que se descartan durante la extracción. ¿Cuál es la razón para tener esto si usamos Coq solo para pruebas? Prop es impredicativo, por lo que Prop: Prop, sin embargo, Coq infiere automáticamente índices de universo y podemos usar Tipo...
Me topé con un desacuerdo confuso entre Agda y Coq que obviamente no está relacionado con las distinciones más conocidas entre sus teorías de tipo (por ejemplo, (im) predicatividad, inducción-recursión, etc.). En particular, Agda acepta la siguiente definición: data Ty : Set0 -> Set0 where...
Dado que no permite el cómputo no determinante, Coq no es necesariamente completo de Turing. ¿Cuál es la clase de funciones que Coq puede calcular? (¿hay una caracterización interesante de los
He visto (y he oído) que afirmaba que es seguro agregar el axioma clásico del medio excluido a Coq, pero parece que no puedo encontrar un documento que respalde esta afirmación. Los documentos que veo enumerados en el wiki de Coq sobre el medio excluido muestran inconsistencia con el conjunto...
¿Hay alguna manera de probar el siguiente teorema en Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. EDITAR : un intento de dar una breve explicación de "qué prueba es irrelevante" (corríjame a alguien si estoy equivocado o es inexacto) La idea básica es que en el mundo...
Coq, Agda e Idris tienen una jerarquía de tipos infinita (Tipo 1: Tipo 2: Tipo 3: ...). Pero, ¿por qué no hacerlo como λC, el sistema en el cubo lambda que está más cerca del cálculo de las construcciones, que tiene solo dos tipos, ∗∗* y , y estas reglas?◽◽◽ ∅ ⊢∗:◽∅⊢∗:◽\frac {} {∅ ⊢ * : ◽} Γ ⊢...
A menudo queremos definir un objeto A∈UA∈UA \in U acuerdo con algunas reglas de inferencia. Dichas normas denotan una función de generación FFF que, cuando es monotónica, se obtiene un punto menos fijo μFμF\mu F . Tomamos A:=μFA:=μFA := \mu F como la "definición inductiva" de AAA . Además, la...
Mientras trato de probar algunas propiedades básicas usando tipos coinductores en Coq, sigo encontrando el siguiente problema y no puedo solucionarlo. He destilado el problema en un simple script Coq de la siguiente manera. El tipo de árbol define árboles posiblemente infinitos con ramas marcadas...
He estado buscando una formalización del teorema de compacidad para FOL, pero no he encontrado ninguna. ¿Alguien está al tanto de tal desarrollo o trabajo
¿Cómo puedo convencer a Coq de que la función recursiva dada a continuación termina? La función toma dos argumentos inductivos. Intuitivamente, la recursión termina porque cualquiera de los argumentos se descompone. Específicamente, la función toma dos árboles como entrada. Inductive Tree := |...
La semántica de un gran subconjunto de OCaml, llamada OCamllight , fue formalizada en HOL por Owens hace varios años. Más recientemente, Kreitz, Hayden y Hickey implementaron una semántica teórica tipo de un subconjunto más pequeño de OCaml en Nuprl . ¿Hay algún desarrollo similar en...
Estoy interesado en modelar objetos, desde la programación orientada a objetos, en la teoría del tipo dependiente. Como posible aplicación, me gustaría tener un modelo donde pueda describir diferentes características de los lenguajes de programación imperativos. Solo pude encontrar un artículo...
He estado programando durante varios años, pero no estoy muy familiarizado con el CS teórico. Recientemente he estado tratando de estudiar lenguajes de programación y, como parte de eso, la verificación de tipos y la inferencia. Mi pregunta es, si trato de escribir una inferencia de tipos y un...
Me preguntaba si el orden de las declaraciones de tipo inductivo puede importar. Por ejemplo, en Coq, puede definir Natya sea por: Inductive Nat := | O : Nat | S : Nat -> Nat. o Inductive Nat := | S : Nat -> Nat | O : Nat. Quizás esto cambie el orden de los parámetros en el...
Quiero saber si la capacidad de decisión de igualdad de dos pruebas decidibles de la misma proposición puede demostrarse sin ningún axioma adicional en el cálculo de construcciones inductivas. Específicamente, quiero saber si esto es cierto sin ningún axioma adicional en Coq. ∀ P: Prop , P∨ ¬ P⇒...
La biblioteca StreamMemo para Coq ilustra cómo memorizar una función f : nat -> Asobre los números naturales. En particular cuando f (S n) = g (f n), imemo_makecomparte el cálculo de llamadas recursivas. Supongamos que, en lugar de números naturales, queremos memorizar funciones recursivas...