coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Wendlasida Ouedraogo <ouedraogo.tertius AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] : Proving "simple lemmas" with Functions or Program fixpoints
- Date: Sun, 22 Aug 2021 17:27:53 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ouedraogo.tertius AT gmail.com; spf=Pass smtp.mailfrom=ouedraogo.tertius AT gmail.com; spf=None smtp.helo=postmaster AT mail-pl1-f176.google.com
- Ironport-hdrordr: A9a23:QsHm/6zg4p36M8y6WjqkKrPwWb1zdoMgy1knxilNoHNuHvBw+/rCoB1k73HJYV8qMRlKpTnqAsa9qB3nn6JI3Q==
- Ironport-phdr: A9a23:F35QnRzoKdxa6J/XCzImylBlVkEcU1XcAAcZ59Idhq5Udez7ptK+ZhSZtKwm0QCBdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekdi72/q29pHObAlFhDiwaq5uIRurqgncqtMYipZ4JKYrzRvJrHpIe+BIym5tOFmegRXy6Nqu8ZB66yhftO4v+MBGUaXhYqQ3VqdYAyg8M2A0/8Lkqx/ORhaS63QGU2UWlh1IAxXZ7Bz/Q5z8vDf2uvZ71SKHO8D9ULI6Vim476pzRxDmiCkJOT0k/m/JlsN9l7hUrA67qhFl34LYfIOYOfxjda3dZ9MaQm9BU95RWCNfBIOzco8PAPAaPeZZsobyvUYFowKjBQayGezv0CVHhnj53a09zu8sFgbG3BE+EN0TqnTbttL1NKgVUeyv0KnH0y/Db+9X2Tfg84jFaR8hofSWUrJxdcrd01UgFwTAjliJr4HuIjya2PgXvWeB8+pgSfygi3QhqwxpvzWiwscih4vKi48Uzl3I6Cp3zYU7K9GlVEN2YN+pHZ9MuiybK4d4Td0vTm92tSs4xLALu4K3cicJxZk52xLRZPqKeJWL7BL7TOudPyt0iXZ/dL+8hxu+61asxvDzW8WuzVpHrCtIn9/RvX4XzRPT8NKISv5l80ehxzmP0wfT5/lBIU8ulKrbL4ctwqY0lpYOqEjDEDL6lUf3gaOMeUUk/e+o6+vjYrr4vJOTK4h0igTmPqQvnMywH/g4PxAQU2SH/emwzr7u8E3jTLlUk/E7nbPVvI3YKMkavqK5BhVa0ocn6xaxFTem19EYkGEALFJYZh2IkpLpNEvJIPD3CvezmUisnylxx/DaP73hH47NI2PMkLfkZ7l96kpcxBAvwtBY4pJYEqsBL+7rWk/tqNzYCQc0PBCzw+b+EdlyyoceWX+UDaKCK6PTsVqI5vo1LOWWZY8Vviz9K/k/6PL0g385gwxVQa781pwOLXu8A/5OIkODYHOqjM1SP30Nu18BQermjFSZUDJaL1GvUq4m7zY0D8ryCprOSpqkh7OGmju2BIFXe3tuBVWFEHOufIKBDaRfIBmOK9Nsx2RXHYOqTJUsgEnGXODSxL9uL+6S8Sod58uLPDld4uTSkVQq8WUxAZ3CjSeCSGZ7mm5OTDgzjvgXSalVxVKK0Kw+iPtdR4Q72g==
Dear List, I am trying to write some proofs for a problem in Coq but I got stuck. My minimized problem is :
-----------------------
Require Import FunInd.
--
Require Import Nat String Recdef Omega.
Function msubstr (s: string) (n : nat) {measure length s} : string :=
if Nat.eqb n 0 then s else
(
match s with
| EmptyString => s
| String h t => msubstr t (n - 1)
end
).
Proof.
intros.
auto.
Qed.
Function msubstr (s: string) (n : nat) {measure length s} : string :=
if Nat.eqb n 0 then s else
(
match s with
| EmptyString => s
| String h t => msubstr t (n - 1)
end
).
Proof.
intros.
auto.
Qed.
-----------------
How to prove : Lemma test: forall a s n, msubstr (String a s) (S n) = msubstr s n.
The general problem is about finding tactics similar to simpl or unfold for Functions and/or Program fixpoints.
Any ideas ?
Regards,
Wendlasida OUEDRAOGO
- [Coq-Club] : Proving "simple lemmas" with Functions or Program fixpoints, Wendlasida Ouedraogo, 08/22/2021
- Re: [Coq-Club] : Proving "simple lemmas" with Functions or Program fixpoints, Castéran Pierre, 08/22/2021
Archive powered by MHonArc 2.6.19+.