Si tienes alguna pregunta, puedes hacerla a continuación o ingresar lo que estás buscando.
¿Existe una buena manera de probar la implementación de una clase en Coq? Por ejemplo, si tengo la siguiente Clase muy simple: El teorema chekc_modulo (c: nat): {c mod 2 = 0} + {c mod 2 <> 0} . Admitido. Definición update(n: nat):= add n one. Clase test :={ f: . . . Read more
Actualmente estoy trabajando en un proyecto en coq donde necesito trabajar con listas de nat -> nat. Básicamente, tengo una definición que toma una lista (nat -> nat) y una proposición f: nat -> nat como parámetros y el objetivo es recuperar el índice de f en la lista dada. . . . Read more
En algunos casos es más fácil instanciar el término existential uno antes que otro. En este ejemplo forzado, deseo establecer c = 3 primero, y de eso elegir, por ejemplo, a = 1 y b = 2. Lema tres_nats: existe (a: nat) (b: nat) (c: nat), a + b = . . . Read more
Supongamos que tengo el siguiente lemma simple y quiero obtener información sobre split. Lemma and_prop: forall (P: Prop) (Q: Prop), P -> Q -> P /\ Q. Proof. intros P Q HP HQ. Info 100 split. lo que produce simple refine ?X10@{__:=P; __:=Q; __:=HP; __:=HQ} ¿Alguien puede explicar qué significa . . . Read more